Theorem mpanr1 431

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 395	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 429	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpanr12  433  axcnre  7616  rec11api  8426  divdiv23apzi  8438  recp1lt1  8567  divgt0i  8578  divge0i  8579  ltreci  8580  lereci  8581  lt2msqi  8582  le2msqi  8583  msq11i  8584  ltdiv23i  8594  ge0gtmnf  9499  sqrt11i  10796  sqrtmuli  10797  sqrtmsq2i  10799  sqrtlei  10800  sqrtlti  10801  cos01gt0  11320