Theorem mp3an3 1316

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  mp3an13  1318  mp3an23  1319  mp3anl3  1323  opelxp  4633  funimaexg  5271  ov  5957  ovmpoa  5968  ovmpo  5973  ovtposg  6223  oaword1  6435  th3q  6602  enrefg  6726  f1imaen  6756  mapxpen  6810  pw1fin  6872  xpfi  6891  djucomen  7168  addnnnq0  7386  mulnnnq0  7387  prarloclemcalc  7439  genpelxp  7448  genpprecll  7451  genppreclu  7452  addsrpr  7682  mulsrpr  7683  gt0srpr  7685  mulid1  7892  ltneg  8356  leneg  8359  suble0  8370  div1  8595  nnaddcl  8873  nnmulcl  8874  nnge1  8876  nnsub  8892  2halves  9082  halfaddsub  9087  addltmul  9089  zleltp1  9242  nnaddm1cl  9248  zextlt  9279  peano5uzti  9295  eluzp1p1  9487  uzaddcl  9520  znq  9558  xrre  9752  xrre2  9753  fzshftral  10039  expn1ap0  10461  expadd  10493  expmul  10496  expubnd  10508  sqmul  10513  bernneq  10571  sqrecapd  10588  faclbnd2  10651  faclbnd6  10653  fihashssdif  10727  shftval3  10765  caucvgre  10919  leabs  11012  ltabs  11025  caubnd2  11055  efexp  11619  efival  11669  cos01gt0  11699  odd2np1  11806  halfleoddlt  11827  omoe  11829  opeo  11830  gcdmultiple  11949  sqgcd  11958  nn0seqcvgd  11969  phiprmpw  12150  eulerthlemth  12160  odzcllem  12170  pcelnn  12248  4sqlem3  12316  ntrin  12724  txuni2  12856  txopn  12865  xblpnfps  12998  xblpnf  12999  bl2in  13003  unirnblps  13022  unirnbl  13023  blpnfctr  13039  sincosq1eq  13360  rpcxpp1  13427  rplogb1  13466