Theorem mpanr1 413

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  mpanr12  415  axcnre  6955  rec11api  7729  divdiv23apzi  7741  recp1lt1  7865  divgt0i  7876  divge0i  7877  ltreci  7878  lereci  7879  lt2msqi  7880  le2msqi  7881  msq11i  7882  ltdiv23i  7892  ge0gtmnf  8736  sqrt11i  9728  sqrtmuli  9729  sqrtmsq2i  9731  sqrtlei  9732  sqrtlti  9733