Theorem mp3an3 1326

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

Hypotheses

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

Assertion

Ref	Expression
mp3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expia 1205	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> th )

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

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 980

This theorem is referenced by:  mp3an13  1328  mp3an23  1329  mp3anl3  1333  opelxp  4654  funimaexg  5297  ov  5989  ovmpoa  6000  ovmpo  6005  ovtposg  6255  oaword1  6467  th3q  6635  enrefg  6759  f1imaen  6789  mapxpen  6843  pw1fin  6905  xpfi  6924  djucomen  7210  addnnnq0  7443  mulnnnq0  7444  prarloclemcalc  7496  genpelxp  7505  genpprecll  7508  genppreclu  7509  addsrpr  7739  mulsrpr  7740  gt0srpr  7742  mulrid  7949  ltneg  8413  leneg  8416  suble0  8427  div1  8654  nnaddcl  8933  nnmulcl  8934  nnge1  8936  nnsub  8952  2halves  9142  halfaddsub  9147  addltmul  9149  zleltp1  9302  nnaddm1cl  9308  zextlt  9339  peano5uzti  9355  eluzp1p1  9547  uzaddcl  9580  znq  9618  xrre  9814  xrre2  9815  fzshftral  10101  expn1ap0  10523  expadd  10555  expmul  10558  expubnd  10570  sqmul  10575  bernneq  10633  sqrecapd  10650  faclbnd2  10713  faclbnd6  10715  fihashssdif  10789  shftval3  10827  caucvgre  10981  leabs  11074  ltabs  11087  caubnd2  11117  efexp  11681  efival  11731  cos01gt0  11761  odd2np1  11868  halfleoddlt  11889  omoe  11891  opeo  11892  gcdmultiple  12011  sqgcd  12020  nn0seqcvgd  12031  phiprmpw  12212  eulerthlemth  12222  odzcllem  12232  pcelnn  12310  4sqlem3  12378  ntrin  13406  txuni2  13538  txopn  13547  xblpnfps  13680  xblpnf  13681  bl2in  13685  unirnblps  13704  unirnbl  13705  blpnfctr  13721  sincosq1eq  14042  rpcxpp1  14109  rplogb1  14148