Theorem mp3an12 1233

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

Syntax hints:   -> wi 4   /\ w3a 896

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

This theorem depends on definitions:  df-bi 114  df-3an 898

This theorem is referenced by:  mp3an12i  1247  ceqsralv  2602  brelrn  4594  funpr  4978  ener  6289  ltaddnq  6562  ltadd1sr  6918  mul02  7455  ltapi  7698  div0ap  7752  divclapzi  7797  divcanap1zi  7798  divcanap2zi  7799  divrecapzi  7800  divcanap3zi  7801  divcanap4zi  7802  divassapzi  7812  divmulapzi  7813  divdirapzi  7814  redivclapzi  7828  ltm1  7886  mulgt1  7903  recgt1i  7938  recreclt  7940  ltmul1i  7960  ltdiv1i  7961  ltmuldivi  7962  ltmul2i  7963  lemul1i  7964  lemul2i  7965  cju  7988  nnge1  8012  nngt0  8014  nnrecgt0  8026  elnnnn0c  8283  elnnz1  8324  recnz  8390  eluzsubi  8595  ge0gtmnf  8836  m1expcl2  9441  1exp  9448  m1expeven  9466  expubnd  9476  iexpcyc  9522  expnbnd  9539  expnlbnd  9540  remim  9687  imval2  9721  cjdivapi  9762  absdivapzi  9980  zeo3  10178  evend2  10200