Theorem mp3an3 1339

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

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

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 983

This theorem is referenced by:  mp3an13  1341  mp3an23  1342  mp3anl3  1346  opelxp  4723  funimaexg  5377  ov  6088  ovmpoa  6099  ovmpo  6104  ovtposg  6368  oaword1  6580  th3q  6750  enrefg  6878  f1imaen  6909  mapxpen  6970  pw1fin  7033  xpfi  7055  djucomen  7359  addnnnq0  7597  mulnnnq0  7598  prarloclemcalc  7650  genpelxp  7659  genpprecll  7662  genppreclu  7663  addsrpr  7893  mulsrpr  7894  gt0srpr  7896  mulrid  8104  ltneg  8570  leneg  8573  suble0  8584  div1  8811  nnaddcl  9091  nnmulcl  9092  nnge1  9094  nnsub  9110  2halves  9301  halfaddsub  9306  addltmul  9309  zleltp1  9463  nnaddm1cl  9469  zextlt  9500  peano5uzti  9516  eluzp1p1  9709  uzaddcl  9742  znq  9780  xrre  9977  xrre2  9978  fzshftral  10265  nninfinf  10625  expn1ap0  10731  expadd  10763  expmul  10766  expubnd  10778  sqmul  10783  bernneq  10842  sqrecapd  10859  faclbnd2  10924  faclbnd6  10926  fihashssdif  11000  ccatlcan  11209  ccatrcan  11210  shftval3  11253  caucvgre  11407  leabs  11500  ltabs  11513  caubnd2  11543  efexp  12108  efival  12158  cos01gt0  12189  odd2np1  12299  halfleoddlt  12320  omoe  12322  opeo  12323  gcdmultiple  12456  sqgcd  12465  nn0seqcvgd  12478  phiprmpw  12659  eulerthlemth  12669  odzcllem  12680  pcelnn  12759  4sqlem3  12828  lsp0  14300  lss0v  14307  zndvds0  14527  ntrin  14711  txuni2  14843  txopn  14852  xblpnfps  14985  xblpnf  14986  bl2in  14990  unirnblps  15009  unirnbl  15010  blpnfctr  15026  plyconst  15332  plyid  15333  sincosq1eq  15426  rpcxpp1  15493  rplogb1  15535