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  4804  funimaexg  5465  ov  6208  ovmpoa  6219  ovmpo  6224  ovtposg  6530  oaword1  6744  th3q  6914  enrefg  7050  f1imaen  7081  mapxpen  7148  pw1fin  7217  xpfi  7239  djucomen  7572  addnnnq0  7816  mulnnnq0  7817  prarloclemcalc  7869  genpelxp  7878  genpprecll  7881  genppreclu  7882  addsrpr  8112  mulsrpr  8113  gt0srpr  8115  mulrid  8323  ltneg  8790  leneg  8793  suble0  8804  div1  9033  nnaddcl  9324  nnmulcl  9325  nnge1  9327  nnsub  9343  2halves  9534  halfaddsub  9539  addltmul  9542  fcdmnn0fsuppg  9618  zleltp1  9700  nnaddm1cl  9706  zextlt  9738  peano5uzti  9754  eluzp1p1  9948  uzaddcl  9986  znq  10024  xrre  10222  xrre2  10223  fzshftral  10515  nninfinf  10880  expn1ap0  10986  expadd  11018  expmul  11021  expubnd  11033  sqmul  11038  bernneq  11098  sqrecapd  11115  faclbnd2  11180  faclbnd6  11182  fihashssdif  11259  ccatlcan  11490  ccatrcan  11491  shftval3  11592  caucvgre  11747  leabs  11840  ltabs  11853  caubnd2  11883  efexp  12449  efival  12499  cos01gt0  12530  odd2np1  12640  halfleoddlt  12661  omoe  12663  opeo  12664  gcdmultiple  12797  sqgcd  12806  nn0seqcvgd  12819  phiprmpw  13000  eulerthlemth  13010  odzcllem  13021  pcelnn  13100  4sqlem3  13169  lsp0  14760  lss0v  14767  zndvds0  14985  ntrin  15225  txuni2  15357  txopn  15366  xblpnfps  15499  xblpnf  15500  bl2in  15504  unirnblps  15523  unirnbl  15524  blpnfctr  15540  plyconst  15846  plyid  15847  sincosq1eq  15940  rpcxpp1  16008  rplogb1  16050