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  4689  funimaexg  5338  ov  6038  ovmpoa  6049  ovmpo  6054  ovtposg  6312  oaword1  6524  th3q  6694  enrefg  6818  f1imaen  6848  mapxpen  6904  pw1fin  6966  xpfi  6986  djucomen  7276  addnnnq0  7509  mulnnnq0  7510  prarloclemcalc  7562  genpelxp  7571  genpprecll  7574  genppreclu  7575  addsrpr  7805  mulsrpr  7806  gt0srpr  7808  mulrid  8016  ltneg  8481  leneg  8484  suble0  8495  div1  8722  nnaddcl  9002  nnmulcl  9003  nnge1  9005  nnsub  9021  2halves  9211  halfaddsub  9216  addltmul  9219  zleltp1  9372  nnaddm1cl  9378  zextlt  9409  peano5uzti  9425  eluzp1p1  9618  uzaddcl  9651  znq  9689  xrre  9886  xrre2  9887  fzshftral  10174  nninfinf  10514  expn1ap0  10620  expadd  10652  expmul  10655  expubnd  10667  sqmul  10672  bernneq  10731  sqrecapd  10748  faclbnd2  10813  faclbnd6  10815  fihashssdif  10889  shftval3  10971  caucvgre  11125  leabs  11218  ltabs  11231  caubnd2  11261  efexp  11825  efival  11875  cos01gt0  11906  odd2np1  12014  halfleoddlt  12035  omoe  12037  opeo  12038  gcdmultiple  12157  sqgcd  12166  nn0seqcvgd  12179  phiprmpw  12360  eulerthlemth  12370  odzcllem  12380  pcelnn  12459  4sqlem3  12528  lsp0  13919  lss0v  13926  zndvds0  14138  ntrin  14292  txuni2  14424  txopn  14433  xblpnfps  14566  xblpnf  14567  bl2in  14571  unirnblps  14590  unirnbl  14591  blpnfctr  14607  plyconst  14891  plyid  14892  sincosq1eq  14974  rpcxpp1  15041  rplogb1  15080