Theorem mp3an12 1273

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

Syntax hints:   -> wi 4   /\ w3a 930

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

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  mp3an12i  1287  ceqsralv  2672  brelrn  4710  funpr  5111  fpm  6505  ener  6603  ltaddnq  7116  ltadd1sr  7472  mul02  8016  ltapi  8263  div0ap  8323  divclapzi  8368  divcanap1zi  8369  divcanap2zi  8370  divrecapzi  8371  divcanap3zi  8372  divcanap4zi  8373  divassapzi  8383  divmulapzi  8384  divdirapzi  8385  redivclapzi  8399  ltm1  8462  mulgt1  8479  recgt1i  8514  recreclt  8516  ltmul1i  8536  ltdiv1i  8537  ltmuldivi  8538  ltmul2i  8539  lemul1i  8540  lemul2i  8541  cju  8577  nnge1  8601  nngt0  8603  nnrecgt0  8616  elnnnn0c  8874  elnnz1  8929  recnz  8996  eluzsubi  9203  ge0gtmnf  9447  m1expcl2  10156  1exp  10163  m1expeven  10181  expubnd  10191  iexpcyc  10238  expnbnd  10256  expnlbnd  10257  remim  10473  imval2  10507  cjdivapi  10548  absdivapzi  10766  ef01bndlem  11261  sin01gt0  11266  cos01gt0  11267  absefib  11274  efieq1re  11275  zeo3  11360  evend2  11381  cnbl0  12456