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  6288  fpmg  6784  pmresg  6786  pw2f1odc  6957  pm54.43  7324  prarloclemarch2  7567  prarloclemlt  7641  prsradd  7934  muleqadd  8776  divdivap1  8831  addltmul  9309  elfzp1b  10254  elfzm1b  10255  expp1zap  10770  expm1ap  10771  fiinbas  14636  opnneissb  14742  blssec  15025