Theorem mpanr2 442

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanr2.1	|- ch
mpanr2.2	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
mpanr2	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mpanr2

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3 |- ch
2	1	jctr 315	. 2 |- ( ps -> ( ps /\ ch ) )
3		mpanr2.2	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	2, 3	sylan2 286	1 |- ( ( ph /\ ps ) -> 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:  op1steq  6413  fpmg  6955  pmresg  6957  pw2f1odc  7135  pm54.43  7536  prarloclemarch2  7786  prarloclemlt  7860  prsradd  8153  muleqadd  9000  divdivap1  9055  addltmul  9546  elfzp1b  10514  elfzm1b  10515  expp1zap  11038  expm1ap  11039  fiinbas  15199  opnneissb  15305  blssec  15588