Theorem mp3an12 1258

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

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  mp3an12i  1272  ceqsralv  2630  brelrn  4585  funpr  4971  ener  6282  ltaddnq  6597  ltadd1sr  6953  mul02  7491  ltapi  7734  div0ap  7790  divclapzi  7835  divcanap1zi  7836  divcanap2zi  7837  divrecapzi  7838  divcanap3zi  7839  divcanap4zi  7840  divassapzi  7850  divmulapzi  7851  divdirapzi  7852  redivclapzi  7866  ltm1  7924  mulgt1  7941  recgt1i  7976  recreclt  7978  ltmul1i  7998  ltdiv1i  7999  ltmuldivi  8000  ltmul2i  8001  lemul1i  8002  lemul2i  8003  cju  8038  nnge1  8062  nngt0  8064  nnrecgt0  8076  elnnnn0c  8333  elnnz1  8374  recnz  8440  eluzsubi  8646  ge0gtmnf  8890  m1expcl2  9498  1exp  9505  m1expeven  9523  expubnd  9533  iexpcyc  9579  expnbnd  9596  expnlbnd  9597  remim  9747  imval2  9781  cjdivapi  9822  absdivapzi  10040  zeo3  10267  evend2  10289