Theorem mp3an12 1364

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

Syntax hints:   -> wi 4   /\ w3a 1005

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

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  mp3an12i  1378  ceqsralv  2847  brelrn  4992  funpr  5410  fpm  6917  ener  7021  0fsupp  7253  ltaddnq  7724  ltadd1sr  8093  map2psrprg  8122  mul02  8662  ltapi  8912  div0ap  8978  divclapzi  9023  divcanap1zi  9024  divcanap2zi  9025  divrecapzi  9026  divcanap3zi  9027  divcanap4zi  9028  divassapzi  9038  divmulapzi  9039  divdirapzi  9040  redivclapzi  9054  ltm1  9122  mulgt1  9139  recgt1i  9174  recreclt  9176  ltmul1i  9196  ltdiv1i  9197  ltmuldivi  9198  ltmul2i  9199  lemul1i  9200  lemul2i  9201  cju  9237  nnge1  9262  nngt0  9264  nnrecgt0  9277  elnnnn0c  9543  elnnz1  9602  recnz  9674  eluzsubi  9885  ge0gtmnf  10159  m1expcl2  10927  1exp  10934  m1expeven  10952  expubnd  10962  iexpcyc  11010  expnbnd  11029  expnlbnd  11030  remim  11549  imval2  11583  cjdivapi  11624  absdivapzi  11843  fprodge1  12329  ef01bndlem  12446  sin01gt0  12452  cos01gt0  12453  cos12dec  12458  absefib  12461  efieq1re  12462  zeo3  12558  evend2  12579  cnbl0  15416  reeff1olem  15653  sincosq1sgn  15708  sincosq3sgn  15710  sincosq4sgn  15711  rpelogb  15831  lgsdir2lem2  15919  konigsberglem5  16504