Theorem mpanr2 438

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 )

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:  op1steq  6323  fpmg  6819  pmresg  6821  pw2f1odc  6992  pm54.43  7359  prarloclemarch2  7602  prarloclemlt  7676  prsradd  7969  muleqadd  8811  divdivap1  8866  addltmul  9344  elfzp1b  10289  elfzm1b  10290  expp1zap  10805  expm1ap  10806  fiinbas  14717  opnneissb  14823  blssec  15106