Theorem mp3an12 1338

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mp3an12.1	|- ph
mp3an12.2	|- ps
mp3an12.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an12	|- ( ch -> th )

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 |- ps
2		mp3an12.1	. . 3 |- ph
3		mp3an12.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an1 1335	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  mp3an12i  1352  ceqsralv  2794  brelrn  4899  funpr  5310  fpm  6740  ener  6838  ltaddnq  7474  ltadd1sr  7843  map2psrprg  7872  mul02  8413  ltapi  8663  div0ap  8729  divclapzi  8774  divcanap1zi  8775  divcanap2zi  8776  divrecapzi  8777  divcanap3zi  8778  divcanap4zi  8779  divassapzi  8789  divmulapzi  8790  divdirapzi  8791  redivclapzi  8805  ltm1  8873  mulgt1  8890  recgt1i  8925  recreclt  8927  ltmul1i  8947  ltdiv1i  8948  ltmuldivi  8949  ltmul2i  8950  lemul1i  8951  lemul2i  8952  cju  8988  nnge1  9013  nngt0  9015  nnrecgt0  9028  elnnnn0c  9294  elnnz1  9349  recnz  9419  eluzsubi  9629  ge0gtmnf  9898  m1expcl2  10653  1exp  10660  m1expeven  10678  expubnd  10688  iexpcyc  10736  expnbnd  10755  expnlbnd  10756  remim  11025  imval2  11059  cjdivapi  11100  absdivapzi  11319  fprodge1  11804  ef01bndlem  11921  sin01gt0  11927  cos01gt0  11928  cos12dec  11933  absefib  11936  efieq1re  11937  zeo3  12033  evend2  12054  cnbl0  14770  reeff1olem  15007  sincosq1sgn  15062  sincosq3sgn  15064  sincosq4sgn  15065  rpelogb  15185  lgsdir2lem2  15270