Theorem mpanr1 437

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
mpanr1	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mpanr1

Step	Hyp	Ref	Expression
1		mpanr1.1	. 2 |- ps
2		mpanr1.2	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	anassrs 400	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  mpanr12  439  axcnre  7994  rec11api  8826  divdiv23apzi  8838  recp1lt1  8972  divgt0i  8983  divge0i  8984  ltreci  8985  lereci  8986  lt2msqi  8987  le2msqi  8988  msq11i  8989  ltdiv23i  8999  ge0gtmnf  9945  sqrt11i  11443  sqrtmuli  11444  sqrtmsq2i  11446  sqrtlei  11447  sqrtlti  11448  cos01gt0  12074