Theorem mp3an3 1360

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 1229	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 15	1 |- ( ( ph /\ ps ) -> 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:  mp3an13  1362  mp3an23  1363  mp3anl3  1367  opelxp  4748  funimaexg  5404  ov  6123  ovmpoa  6134  ovmpo  6139  ovtposg  6403  oaword1  6615  th3q  6785  enrefg  6913  f1imaen  6944  mapxpen  7005  pw1fin  7068  xpfi  7090  djucomen  7394  addnnnq0  7632  mulnnnq0  7633  prarloclemcalc  7685  genpelxp  7694  genpprecll  7697  genppreclu  7698  addsrpr  7928  mulsrpr  7929  gt0srpr  7931  mulrid  8139  ltneg  8605  leneg  8608  suble0  8619  div1  8846  nnaddcl  9126  nnmulcl  9127  nnge1  9129  nnsub  9145  2halves  9336  halfaddsub  9341  addltmul  9344  zleltp1  9498  nnaddm1cl  9504  zextlt  9535  peano5uzti  9551  eluzp1p1  9744  uzaddcl  9777  znq  9815  xrre  10012  xrre2  10013  fzshftral  10300  nninfinf  10660  expn1ap0  10766  expadd  10798  expmul  10801  expubnd  10813  sqmul  10818  bernneq  10877  sqrecapd  10894  faclbnd2  10959  faclbnd6  10961  fihashssdif  11035  ccatlcan  11245  ccatrcan  11246  shftval3  11333  caucvgre  11487  leabs  11580  ltabs  11593  caubnd2  11623  efexp  12188  efival  12238  cos01gt0  12269  odd2np1  12379  halfleoddlt  12400  omoe  12402  opeo  12403  gcdmultiple  12536  sqgcd  12545  nn0seqcvgd  12558  phiprmpw  12739  eulerthlemth  12749  odzcllem  12760  pcelnn  12839  4sqlem3  12908  lsp0  14381  lss0v  14388  zndvds0  14608  ntrin  14792  txuni2  14924  txopn  14933  xblpnfps  15066  xblpnf  15067  bl2in  15071  unirnblps  15090  unirnbl  15091  blpnfctr  15107  plyconst  15413  plyid  15414  sincosq1eq  15507  rpcxpp1  15574  rplogb1  15616