Theorem mp3an12 1322

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

Syntax hints:   -> wi 4   /\ w3a 973

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

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

This theorem is referenced by:  mp3an12i  1336  ceqsralv  2761  brelrn  4842  funpr  5248  fpm  6655  ener  6753  ltaddnq  7356  ltadd1sr  7725  map2psrprg  7754  mul02  8293  ltapi  8542  div0ap  8606  divclapzi  8651  divcanap1zi  8652  divcanap2zi  8653  divrecapzi  8654  divcanap3zi  8655  divcanap4zi  8656  divassapzi  8666  divmulapzi  8667  divdirapzi  8668  redivclapzi  8682  ltm1  8749  mulgt1  8766  recgt1i  8801  recreclt  8803  ltmul1i  8823  ltdiv1i  8824  ltmuldivi  8825  ltmul2i  8826  lemul1i  8827  lemul2i  8828  cju  8864  nnge1  8888  nngt0  8890  nnrecgt0  8903  elnnnn0c  9167  elnnz1  9222  recnz  9292  eluzsubi  9501  ge0gtmnf  9767  m1expcl2  10485  1exp  10492  m1expeven  10510  expubnd  10520  iexpcyc  10567  expnbnd  10586  expnlbnd  10587  remim  10811  imval2  10845  cjdivapi  10886  absdivapzi  11105  fprodge1  11589  ef01bndlem  11706  sin01gt0  11711  cos01gt0  11712  cos12dec  11717  absefib  11720  efieq1re  11721  zeo3  11814  evend2  11835  cnbl0  13287  reeff1olem  13445  sincosq1sgn  13500  sincosq3sgn  13502  sincosq4sgn  13503  rpelogb  13620  lgsdir2lem2  13683