Theorem mp3an12 1368

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  mp3an12i  1382  ceqsralv  2853  brelrn  5010  funpr  5428  fpm  6952  ener  7056  0fsupp  7288  ltaddnq  7764  ltadd1sr  8133  map2psrprg  8162  mul02  8704  ltapi  8954  div0ap  9022  divclapzi  9067  divcanap1zi  9068  divcanap2zi  9069  divrecapzi  9070  divcanap3zi  9071  divcanap4zi  9072  divassapzi  9082  divmulapzi  9083  divdirapzi  9084  redivclapzi  9098  ltm1  9166  mulgt1  9183  recgt1i  9218  recreclt  9220  ltmul1i  9240  ltdiv1i  9241  ltmuldivi  9242  ltmul2i  9243  lemul1i  9244  lemul2i  9245  cju  9281  nnge1  9306  nngt0  9308  nnrecgt0  9321  elnnnn0c  9587  elnnz1  9646  recnz  9718  eluzsubi  9929  ge0gtmnf  10204  m1expcl2  10976  1exp  10983  m1expeven  11001  expubnd  11011  iexpcyc  11059  resq01  11073  expnbnd  11079  expnlbnd  11080  remim  11603  imval2  11637  cjdivapi  11679  absdivapzi  11898  fprodge1  12384  ef01bndlem  12501  sin01gt0  12507  cos01gt0  12508  cos12dec  12513  absefib  12516  efieq1re  12517  zeo3  12613  evend2  12634  cnbl0  15558  reeff1olem  15795  sincosq1sgn  15850  sincosq3sgn  15852  sincosq4sgn  15853  rpelogb  15974  lgsdir2lem2  16062  konigsberglem5  16647