Theorem mp3an2 1256

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
mp3an2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1138	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 425	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mp3anl2  1263  ordin  4140  ordsuc  4306  omv  6058  oeiv  6059  omv2  6068  1idprl  6780  muladd11  7241  negsub  7356  subneg  7357  ltaddneg  7528  muleqadd  7758  diveqap1  7793  conjmulap  7817  nnsub  8077  addltmul  8267  zltp1le  8405  gtndiv  8442  eluzp1m1  8642  divelunit  9024  fznatpl1  9093  flqbi2  9293  flqdiv  9323  frecfzen2  9420  nn0ennn  9425  iseqshft2  9452  faclbnd3  9670  shftfvalg  9706  ovshftex  9707  shftfval  9709  abs2dif  9992  omeo  10298  gcd0id  10370  sqgcd  10418  isprm3  10500