Theorem mpanr2 434

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 313	. 2 |- ( ps -> ( ps /\ ch ) )
3		mpanr2.2	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
4	2, 3	sylan2 284	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  op1steq  6077  fpmg  6568  pmresg  6570  pm54.43  7046  prarloclemarch2  7227  prarloclemlt  7301  prsradd  7594  muleqadd  8429  divdivap1  8483  addltmul  8956  elfzp1b  9877  elfzm1b  9878  expp1zap  10342  expm1ap  10343  fiinbas  12216  opnneissb  12324  blssec  12607