Theorem mp3an3 1326

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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 980

This theorem is referenced by:  mp3an13  1328  mp3an23  1329  mp3anl3  1333  opelxp  4656  funimaexg  5300  ov  5993  ovmpoa  6004  ovmpo  6009  ovtposg  6259  oaword1  6471  th3q  6639  enrefg  6763  f1imaen  6793  mapxpen  6847  pw1fin  6909  xpfi  6928  djucomen  7214  addnnnq0  7447  mulnnnq0  7448  prarloclemcalc  7500  genpelxp  7509  genpprecll  7512  genppreclu  7513  addsrpr  7743  mulsrpr  7744  gt0srpr  7746  mulrid  7953  ltneg  8418  leneg  8421  suble0  8432  div1  8659  nnaddcl  8938  nnmulcl  8939  nnge1  8941  nnsub  8957  2halves  9147  halfaddsub  9152  addltmul  9154  zleltp1  9307  nnaddm1cl  9313  zextlt  9344  peano5uzti  9360  eluzp1p1  9552  uzaddcl  9585  znq  9623  xrre  9819  xrre2  9820  fzshftral  10107  expn1ap0  10529  expadd  10561  expmul  10564  expubnd  10576  sqmul  10581  bernneq  10640  sqrecapd  10657  faclbnd2  10721  faclbnd6  10723  fihashssdif  10797  shftval3  10835  caucvgre  10989  leabs  11082  ltabs  11095  caubnd2  11125  efexp  11689  efival  11739  cos01gt0  11769  odd2np1  11877  halfleoddlt  11898  omoe  11900  opeo  11901  gcdmultiple  12020  sqgcd  12029  nn0seqcvgd  12040  phiprmpw  12221  eulerthlemth  12231  odzcllem  12241  pcelnn  12319  4sqlem3  12387  ntrin  13594  txuni2  13726  txopn  13735  xblpnfps  13868  xblpnf  13869  bl2in  13873  unirnblps  13892  unirnbl  13893  blpnfctr  13909  sincosq1eq  14230  rpcxpp1  14297  rplogb1  14336