Theorem mp3an2 1362

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 1230	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 435	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005

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 depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  mp3anl2  1369  ordin  4511  ordsuc  4690  omv  6701  oeiv  6702  omv2  6711  1idprl  7921  muladd11  8423  negsub  8538  subneg  8539  ltaddneg  8716  muleqadd  8962  diveqap1  8999  conjmulap  9023  nnsub  9296  addltmul  9495  zltp1le  9652  gtndiv  9694  eluzp1m1  9899  xnn0le2is012  10221  divelunit  10357  fznatpl1  10435  flqbi2  10678  flqdiv  10710  frecfzen2  10816  nn0ennn  10822  seqshft2g  10871  seqf1oglem1  10908  faclbnd3  11133  ccatrid  11323  shftfvalg  11531  ovshftex  11532  shftfval  11534  abs2dif  11819  cos2t  12464  sin01gt0  12476  cos01gt0  12477  demoivre  12487  demoivreALT  12488  omeo  12612  gcd0id  12703  sqgcd  12753  isprm3  12843  eulerthlemth  12957  pczpre  13023  pcrec  13034  setscom  13339  setsslid  13350  setsslnid  13351  mulgm1  13898  abssinper  15840  lgs1  16046