Theorem mp3an12 1368

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12i  1382  ceqsralv  2853  brelrn  5017  funpr  5436  fpm  6967  ener  7072  ltaddnq  7780  ltadd1sr  8149  map2psrprg  8178  mul02  8721  ltapi  8972  div0ap  9040  divclapzi  9085  divcanap1zi  9086  divcanap2zi  9087  divrecapzi  9088  divcanap3zi  9089  divcanap4zi  9090  divassapzi  9100  divmulapzi  9101  divdirapzi  9102  redivclapzi  9116  ltm1  9184  mulgt1  9201  recgt1i  9236  recreclt  9238  ltmul1i  9258  ltdiv1i  9259  ltmuldivi  9260  ltmul2i  9261  lemul1i  9262  lemul2i  9263  cju  9299  nnge1  9336  nngt0  9338  nnrecgt0  9351  elnnnn0c  9619  elnnz1  9676  recnz  9749  eluzsubi  9965  ge0gtmnf  10241  m1expcl2  11018  1exp  11025  m1expeven  11043  expubnd  11053  iexpcyc  11101  resq01  11115  expnbnd  11121  expnlbnd  11122  remim  11646  imval2  11680  cjdivapi  11722  absdivapzi  11942  fprodge1  12430  ef01bndlem  12547  sin01gt0  12553  cos01gt0  12554  cos12dec  12559  absefib  12562  efieq1re  12563  zeo3  12659  evend2  12680  prmlem1  13250  prmlem2  13262  cnbl0  15777  reeff1olem  16014  sincosq1sgn  16070  sincosq3sgn  16072  sincosq4sgn  16073  sineq0re  16093  rpelogb  16202  bposlem8  16335  lgsdir2lem2  16370  konigsberglem5  16955