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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  mpanr12  443  axcnre  8249  rec11api  9086  divdiv23apzi  9098  recp1lt1  9232  divgt0i  9243  divge0i  9244  ltreci  9245  lereci  9246  lt2msqi  9247  le2msqi  9248  msq11i  9249  ltdiv23i  9259  ge0gtmnf  10236  sqrt11i  11915  sqrtmuli  11916  sqrtmsq2i  11918  sqrtlei  11919  sqrtlti  11920  cos01gt0  12549