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  4690  funimaexg  5339  ov  6039  ovmpoa  6050  ovmpo  6055  ovtposg  6314  oaword1  6526  th3q  6696  enrefg  6820  f1imaen  6850  mapxpen  6906  pw1fin  6968  xpfi  6988  djucomen  7278  addnnnq0  7511  mulnnnq0  7512  prarloclemcalc  7564  genpelxp  7573  genpprecll  7576  genppreclu  7577  addsrpr  7807  mulsrpr  7808  gt0srpr  7810  mulrid  8018  ltneg  8483  leneg  8486  suble0  8497  div1  8724  nnaddcl  9004  nnmulcl  9005  nnge1  9007  nnsub  9023  2halves  9214  halfaddsub  9219  addltmul  9222  zleltp1  9375  nnaddm1cl  9381  zextlt  9412  peano5uzti  9428  eluzp1p1  9621  uzaddcl  9654  znq  9692  xrre  9889  xrre2  9890  fzshftral  10177  nninfinf  10517  expn1ap0  10623  expadd  10655  expmul  10658  expubnd  10670  sqmul  10675  bernneq  10734  sqrecapd  10751  faclbnd2  10816  faclbnd6  10818  fihashssdif  10892  shftval3  10974  caucvgre  11128  leabs  11221  ltabs  11234  caubnd2  11264  efexp  11828  efival  11878  cos01gt0  11909  odd2np1  12017  halfleoddlt  12038  omoe  12040  opeo  12041  gcdmultiple  12160  sqgcd  12169  nn0seqcvgd  12182  phiprmpw  12363  eulerthlemth  12373  odzcllem  12383  pcelnn  12462  4sqlem3  12531  lsp0  13922  lss0v  13929  zndvds0  14149  ntrin  14303  txuni2  14435  txopn  14444  xblpnfps  14577  xblpnf  14578  bl2in  14582  unirnblps  14601  unirnbl  14602  blpnfctr  14618  plyconst  14924  plyid  14925  sincosq1eq  15015  rpcxpp1  15082  rplogb1  15121