Theorem mpan2i 701

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mpan2i.1	|- ch
mpan2i.2	|- (ph -> ((ps /\ ch) -> th))

Assertion

Ref	Expression
mpan2i	|- (ph -> (ps -> th))

Proof of Theorem mpan2i

Step	Hyp	Ref	Expression
1		mpan2i.1	. 2 |- ch
2		mpan2i.2	. . 3 |- (ph -> ((ps /\ ch) -> th))
3	2	exp3a 376	. 2 |- (ph -> (ps -> (ch -> th)))
4	1, 3	mpii 45	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  mpanr2 712  sdomsdomcard 4859  cflecard 4924  genpprecl 5116  nnleltp1t 5956  lt0nnn0 6118  sqrlem6 6679  sqrlem12 6685  sqr00t 6715  pilem1 8666  pilem2 8667  sincosq1lem 8698  mdsl1 10243

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain