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  4657  funimaexg  5301  ov  5994  ovmpoa  6005  ovmpo  6010  ovtposg  6260  oaword1  6472  th3q  6640  enrefg  6764  f1imaen  6794  mapxpen  6848  pw1fin  6910  xpfi  6929  djucomen  7215  addnnnq0  7448  mulnnnq0  7449  prarloclemcalc  7501  genpelxp  7510  genpprecll  7513  genppreclu  7514  addsrpr  7744  mulsrpr  7745  gt0srpr  7747  mulrid  7954  ltneg  8419  leneg  8422  suble0  8433  div1  8660  nnaddcl  8939  nnmulcl  8940  nnge1  8942  nnsub  8958  2halves  9148  halfaddsub  9153  addltmul  9155  zleltp1  9308  nnaddm1cl  9314  zextlt  9345  peano5uzti  9361  eluzp1p1  9553  uzaddcl  9586  znq  9624  xrre  9820  xrre2  9821  fzshftral  10108  expn1ap0  10530  expadd  10562  expmul  10565  expubnd  10577  sqmul  10582  bernneq  10641  sqrecapd  10658  faclbnd2  10722  faclbnd6  10724  fihashssdif  10798  shftval3  10836  caucvgre  10990  leabs  11083  ltabs  11096  caubnd2  11126  efexp  11690  efival  11740  cos01gt0  11770  odd2np1  11878  halfleoddlt  11899  omoe  11901  opeo  11902  gcdmultiple  12021  sqgcd  12030  nn0seqcvgd  12041  phiprmpw  12222  eulerthlemth  12232  odzcllem  12242  pcelnn  12320  4sqlem3  12388  ntrin  13627  txuni2  13759  txopn  13768  xblpnfps  13901  xblpnf  13902  bl2in  13906  unirnblps  13925  unirnbl  13926  blpnfctr  13942  sincosq1eq  14263  rpcxpp1  14330  rplogb1  14369