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  4844  funpr  5250  fpm  6659  ener  6757  ltaddnq  7369  ltadd1sr  7738  map2psrprg  7767  mul02  8306  ltapi  8555  div0ap  8619  divclapzi  8664  divcanap1zi  8665  divcanap2zi  8666  divrecapzi  8667  divcanap3zi  8668  divcanap4zi  8669  divassapzi  8679  divmulapzi  8680  divdirapzi  8681  redivclapzi  8695  ltm1  8762  mulgt1  8779  recgt1i  8814  recreclt  8816  ltmul1i  8836  ltdiv1i  8837  ltmuldivi  8838  ltmul2i  8839  lemul1i  8840  lemul2i  8841  cju  8877  nnge1  8901  nngt0  8903  nnrecgt0  8916  elnnnn0c  9180  elnnz1  9235  recnz  9305  eluzsubi  9514  ge0gtmnf  9780  m1expcl2  10498  1exp  10505  m1expeven  10523  expubnd  10533  iexpcyc  10580  expnbnd  10599  expnlbnd  10600  remim  10824  imval2  10858  cjdivapi  10899  absdivapzi  11118  fprodge1  11602  ef01bndlem  11719  sin01gt0  11724  cos01gt0  11725  cos12dec  11730  absefib  11733  efieq1re  11734  zeo3  11827  evend2  11848  cnbl0  13328  reeff1olem  13486  sincosq1sgn  13541  sincosq3sgn  13543  sincosq4sgn  13544  rpelogb  13661  lgsdir2lem2  13724