Theorem mp3an3 1362

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

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

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 1006

This theorem is referenced by:  mp3an13  1364  mp3an23  1365  mp3anl3  1369  opelxp  4755  funimaexg  5414  ov  6144  ovmpoa  6155  ovmpo  6160  ovtposg  6428  oaword1  6642  th3q  6812  enrefg  6940  f1imaen  6971  mapxpen  7037  pw1fin  7105  xpfi  7127  djucomen  7434  addnnnq0  7672  mulnnnq0  7673  prarloclemcalc  7725  genpelxp  7734  genpprecll  7737  genppreclu  7738  addsrpr  7968  mulsrpr  7969  gt0srpr  7971  mulrid  8179  ltneg  8645  leneg  8648  suble0  8659  div1  8886  nnaddcl  9166  nnmulcl  9167  nnge1  9169  nnsub  9185  2halves  9376  halfaddsub  9381  addltmul  9384  zleltp1  9538  nnaddm1cl  9544  zextlt  9575  peano5uzti  9591  eluzp1p1  9785  uzaddcl  9823  znq  9861  xrre  10058  xrre2  10059  fzshftral  10346  nninfinf  10709  expn1ap0  10815  expadd  10847  expmul  10850  expubnd  10862  sqmul  10867  bernneq  10926  sqrecapd  10943  faclbnd2  11008  faclbnd6  11010  fihashssdif  11086  ccatlcan  11306  ccatrcan  11307  shftval3  11408  caucvgre  11562  leabs  11655  ltabs  11668  caubnd2  11698  efexp  12264  efival  12314  cos01gt0  12345  odd2np1  12455  halfleoddlt  12476  omoe  12478  opeo  12479  gcdmultiple  12612  sqgcd  12621  nn0seqcvgd  12634  phiprmpw  12815  eulerthlemth  12825  odzcllem  12836  pcelnn  12915  4sqlem3  12984  lsp0  14459  lss0v  14466  zndvds0  14686  ntrin  14875  txuni2  15007  txopn  15016  xblpnfps  15149  xblpnf  15150  bl2in  15154  unirnblps  15173  unirnbl  15174  blpnfctr  15190  plyconst  15496  plyid  15497  sincosq1eq  15590  rpcxpp1  15657  rplogb1  15699