Theorem mp3an3 1337

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 1207	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> th )

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

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 982

This theorem is referenced by:  mp3an13  1339  mp3an23  1340  mp3anl3  1344  opelxp  4681  funimaexg  5326  ov  6024  ovmpoa  6035  ovmpo  6040  ovtposg  6292  oaword1  6504  th3q  6674  enrefg  6798  f1imaen  6828  mapxpen  6884  pw1fin  6946  xpfi  6966  djucomen  7255  addnnnq0  7488  mulnnnq0  7489  prarloclemcalc  7541  genpelxp  7550  genpprecll  7553  genppreclu  7554  addsrpr  7784  mulsrpr  7785  gt0srpr  7787  mulrid  7995  ltneg  8460  leneg  8463  suble0  8474  div1  8701  nnaddcl  8980  nnmulcl  8981  nnge1  8983  nnsub  8999  2halves  9189  halfaddsub  9194  addltmul  9196  zleltp1  9349  nnaddm1cl  9355  zextlt  9386  peano5uzti  9402  eluzp1p1  9595  uzaddcl  9628  znq  9666  xrre  9862  xrre2  9863  fzshftral  10150  nninfinf  10486  expn1ap0  10576  expadd  10608  expmul  10611  expubnd  10623  sqmul  10628  bernneq  10687  sqrecapd  10704  faclbnd2  10769  faclbnd6  10771  fihashssdif  10845  shftval3  10883  caucvgre  11037  leabs  11130  ltabs  11143  caubnd2  11173  efexp  11737  efival  11787  cos01gt0  11817  odd2np1  11925  halfleoddlt  11946  omoe  11948  opeo  11949  gcdmultiple  12068  sqgcd  12077  nn0seqcvgd  12090  phiprmpw  12271  eulerthlemth  12281  odzcllem  12291  pcelnn  12370  4sqlem3  12439  lsp0  13782  lss0v  13789  zndvds0  13994  ntrin  14145  txuni2  14277  txopn  14286  xblpnfps  14419  xblpnf  14420  bl2in  14424  unirnblps  14443  unirnbl  14444  blpnfctr  14460  sincosq1eq  14798  rpcxpp1  14865  rplogb1  14904