Theorem mp3an12 1361

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 1358	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 424	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  mp3an12i  1375  ceqsralv  2831  brelrn  4957  funpr  5373  fpm  6828  ener  6931  ltaddnq  7594  ltadd1sr  7963  map2psrprg  7992  mul02  8533  ltapi  8783  div0ap  8849  divclapzi  8894  divcanap1zi  8895  divcanap2zi  8896  divrecapzi  8897  divcanap3zi  8898  divcanap4zi  8899  divassapzi  8909  divmulapzi  8910  divdirapzi  8911  redivclapzi  8925  ltm1  8993  mulgt1  9010  recgt1i  9045  recreclt  9047  ltmul1i  9067  ltdiv1i  9068  ltmuldivi  9069  ltmul2i  9070  lemul1i  9071  lemul2i  9072  cju  9108  nnge1  9133  nngt0  9135  nnrecgt0  9148  elnnnn0c  9414  elnnz1  9469  recnz  9540  eluzsubi  9750  ge0gtmnf  10019  m1expcl2  10783  1exp  10790  m1expeven  10808  expubnd  10818  iexpcyc  10866  expnbnd  10885  expnlbnd  10886  remim  11371  imval2  11405  cjdivapi  11446  absdivapzi  11665  fprodge1  12150  ef01bndlem  12267  sin01gt0  12273  cos01gt0  12274  cos12dec  12279  absefib  12282  efieq1re  12283  zeo3  12379  evend2  12400  cnbl0  15208  reeff1olem  15445  sincosq1sgn  15500  sincosq3sgn  15502  sincosq4sgn  15503  rpelogb  15623  lgsdir2lem2  15708