Theorem mp3an2 1359

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

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

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 1004

This theorem is referenced by:  mp3anl2  1366  ordin  4480  ordsuc  4659  omv  6618  oeiv  6619  omv2  6628  1idprl  7803  muladd11  8305  negsub  8420  subneg  8421  ltaddneg  8597  muleqadd  8841  diveqap1  8878  conjmulap  8902  nnsub  9175  addltmul  9374  zltp1le  9527  gtndiv  9568  eluzp1m1  9773  xnn0le2is012  10094  divelunit  10230  fznatpl1  10304  flqbi2  10544  flqdiv  10576  frecfzen2  10682  nn0ennn  10688  seqshft2g  10737  seqf1oglem1  10774  faclbnd3  10998  ccatrid  11177  shftfvalg  11372  ovshftex  11373  shftfval  11375  abs2dif  11660  cos2t  12304  sin01gt0  12316  cos01gt0  12317  demoivre  12327  demoivreALT  12328  omeo  12452  gcd0id  12543  sqgcd  12593  isprm3  12683  eulerthlemth  12797  pczpre  12863  pcrec  12874  setscom  13115  setsslid  13126  setsslnid  13127  mulgm1  13722  abssinper  15563  lgs1  15766