Theorem mp3an3 1363

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 1232	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> 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:  mp3an13  1365  mp3an23  1366  mp3anl3  1370  opelxp  4781  funimaexg  5442  ov  6175  ovmpoa  6186  ovmpo  6191  ovtposg  6492  oaword1  6706  th3q  6876  enrefg  7005  f1imaen  7036  mapxpen  7103  pw1fin  7172  xpfi  7194  djucomen  7525  addnnnq0  7766  mulnnnq0  7767  prarloclemcalc  7819  genpelxp  7828  genpprecll  7831  genppreclu  7832  addsrpr  8062  mulsrpr  8063  gt0srpr  8065  mulrid  8273  ltneg  8738  leneg  8741  suble0  8752  div1  8979  nnaddcl  9259  nnmulcl  9260  nnge1  9262  nnsub  9278  2halves  9469  halfaddsub  9474  addltmul  9477  fcdmnn0fsuppg  9553  zleltp1  9635  nnaddm1cl  9641  zextlt  9673  peano5uzti  9689  eluzp1p1  9883  uzaddcl  9921  znq  9959  xrre  10156  xrre2  10157  fzshftral  10446  nninfinf  10809  expn1ap0  10915  expadd  10947  expmul  10950  expubnd  10962  sqmul  10967  bernneq  11026  sqrecapd  11043  faclbnd2  11108  faclbnd6  11110  fihashssdif  11187  ccatlcan  11414  ccatrcan  11415  shftval3  11516  caucvgre  11670  leabs  11763  ltabs  11776  caubnd2  11806  efexp  12372  efival  12422  cos01gt0  12453  odd2np1  12563  halfleoddlt  12584  omoe  12586  opeo  12587  gcdmultiple  12720  sqgcd  12729  nn0seqcvgd  12742  phiprmpw  12923  eulerthlemth  12933  odzcllem  12944  pcelnn  13023  4sqlem3  13092  lsp0  14588  lss0v  14595  zndvds0  14815  ntrin  15006  txuni2  15138  txopn  15147  xblpnfps  15280  xblpnf  15281  bl2in  15285  unirnblps  15304  unirnbl  15305  blpnfctr  15321  plyconst  15627  plyid  15628  sincosq1eq  15721  rpcxpp1  15788  rplogb1  15830