Theorem mp3an12 1259

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

Syntax hints:   -> wi 4   /\ w3a 920

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 922

This theorem is referenced by:  mp3an12i  1273  ceqsralv  2639  brelrn  4615  funpr  5002  ener  6348  ltaddnq  6729  ltadd1sr  7085  mul02  7628  ltapi  7871  div0ap  7927  divclapzi  7972  divcanap1zi  7973  divcanap2zi  7974  divrecapzi  7975  divcanap3zi  7976  divcanap4zi  7977  divassapzi  7987  divmulapzi  7988  divdirapzi  7989  redivclapzi  8003  ltm1  8061  mulgt1  8078  recgt1i  8113  recreclt  8115  ltmul1i  8135  ltdiv1i  8136  ltmuldivi  8137  ltmul2i  8138  lemul1i  8139  lemul2i  8140  cju  8175  nnge1  8199  nngt0  8201  nnrecgt0  8213  elnnnn0c  8470  elnnz1  8525  recnz  8591  eluzsubi  8797  ge0gtmnf  9036  m1expcl2  9665  1exp  9672  m1expeven  9690  expubnd  9700  iexpcyc  9746  expnbnd  9763  expnlbnd  9764  remim  9966  imval2  10000  cjdivapi  10041  absdivapzi  10259  zeo3  10493  evend2  10514