Theorem mp3an3 1367

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4806  funimaexg  5468  ov  6211  ovmpoa  6222  ovmpo  6227  ovtposg  6534  oaword1  6748  th3q  6918  enrefg  7054  f1imaen  7085  mapxpen  7152  pw1fin  7221  xpfi  7243  djucomen  7578  addnnnq0  7822  mulnnnq0  7823  prarloclemcalc  7875  genpelxp  7884  genpprecll  7887  genppreclu  7888  addsrpr  8118  mulsrpr  8119  gt0srpr  8121  mulrid  8329  ltneg  8797  leneg  8800  suble0  8811  div1  9041  nnaddcl  9333  nnmulcl  9334  nnge1  9336  nnsub  9352  2halves  9545  halfaddsub  9550  addltmul  9553  fcdmnn0fsuppg  9629  zleltp1  9711  nnaddm1cl  9717  zextlt  9749  peano5uzti  9765  eluzp1p1  9964  uzaddcl  10002  znq  10040  xrre  10239  xrre2  10240  fzshftral  10532  nninfinf  10901  expn1ap0  11007  expadd  11039  expmul  11042  expubnd  11054  sqmul  11059  bernneq  11119  sqrecapd  11136  faclbnd2  11202  faclbnd6  11204  fihashssdif  11281  ccatlcan  11512  ccatrcan  11513  shftval3  11614  caucvgre  11769  leabs  11862  ltabs  11876  caubnd2  11906  efexp  12474  efival  12524  cos01gt0  12555  odd2np1  12665  halfleoddlt  12686  omoe  12688  opeo  12689  gcdmultiple  12822  sqgcd  12831  nn0seqcvgd  12844  phiprmpw  13029  eulerthlemth  13039  odzcllem  13050  pcelnn  13129  4sqlem3  13198  lsp0  14869  lss0v  14876  zndvds0  15094  ntrin  15350  txuni2  15482  txopn  15491  xblpnfps  15624  xblpnf  15625  bl2in  15629  unirnblps  15648  unirnbl  15649  blpnfctr  15665  plyconst  15971  plyid  15972  sincosq1eq  16066  rpcxpp1  16139  rplogb1  16184  ppiqub  16293  bposlem1  16311  bposlem2  16312  bposlem9  16319