Theorem mpanr1 428

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mpanr12  430  axcnre  7179  rec11api  7978  divdiv23apzi  7990  recp1lt1  8114  divgt0i  8125  divge0i  8126  ltreci  8127  lereci  8128  lt2msqi  8129  le2msqi  8130  msq11i  8131  ltdiv23i  8141  ge0gtmnf  9036  sqrt11i  10237  sqrtmuli  10238  sqrtmsq2i  10240  sqrtlei  10241  sqrtlti  10242