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  6070  fpmg  6561  pmresg  6563  pm54.43  7039  prarloclemarch2  7220  prarloclemlt  7294  prsradd  7587  muleqadd  8422  divdivap1  8476  addltmul  8949  elfzp1b  9870  elfzm1b  9871  expp1zap  10335  expm1ap  10336  fiinbas  12205  opnneissb  12313  blssec  12596