Theorem mp3an3 1257

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mp3an13  1259  mp3an23  1260  mp3anl3  1264  opelxp  4392  funimaexg  5003  ov  5640  ovmpt2a  5651  ovmpt2  5656  ovtposg  5897  oaword1  6073  th3q  6234  enrefg  6267  f1imaen  6297  addnnnq0  6639  mulnnnq0  6640  prarloclemcalc  6692  genpelxp  6701  genpprecll  6704  genppreclu  6705  addsrpr  6922  mulsrpr  6923  gt0srpr  6925  mulid1  7116  ltneg  7566  leneg  7569  suble0  7580  div1  7791  nnaddcl  8059  nnmulcl  8060  nnge1  8062  nnsub  8077  2halves  8260  halfaddsub  8265  addltmul  8267  zleltp1  8406  nnaddm1cl  8412  zextlt  8439  peano5uzti  8455  eluzp1p1  8644  uzaddcl  8674  znq  8709  xrre  8887  xrre2  8888  fzshftral  9125  expn1ap0  9486  expadd  9518  expmul  9521  expubnd  9533  sqmul  9538  bernneq  9593  sqrecapd  9609  faclbnd2  9669  faclbnd6  9671  shftval3  9715  caucvgre  9867  leabs  9960  ltabs  9973  caubnd2  10003  odd2np1  10272  halfleoddlt  10294  omoe  10296  opeo  10297  gcdmultiple  10409  sqgcd  10418  nn0seqcvgd  10423