Theorem mpanr1 441

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 404	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 439	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  443  axcnre  8238  rec11api  9073  divdiv23apzi  9085  recp1lt1  9219  divgt0i  9230  divge0i  9231  ltreci  9232  lereci  9233  lt2msqi  9234  le2msqi  9235  msq11i  9236  ltdiv23i  9246  ge0gtmnf  10204  sqrt11i  11876  sqrtmuli  11877  sqrtmsq2i  11879  sqrtlei  11880  sqrtlti  11881  cos01gt0  12508