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  6966  ener  7070  0fsupp  7303  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  9678  recnz  9750  eluzsubi  9966  ge0gtmnf  10242  m1expcl2  11019  1exp  11026  m1expeven  11044  expubnd  11054  iexpcyc  11102  resq01  11116  expnbnd  11122  expnlbnd  11123  remim  11647  imval2  11681  cjdivapi  11723  absdivapzi  11943  fprodge1  12431  ef01bndlem  12548  sin01gt0  12554  cos01gt0  12555  cos12dec  12560  absefib  12563  efieq1re  12564  zeo3  12660  evend2  12681  prmlem1  13251  prmlem2  13263  cnbl0  15760  reeff1olem  15997  sincosq1sgn  16053  sincosq3sgn  16055  sincosq4sgn  16056  sineq0re  16076  rpelogb  16185  bposlem8  16318  lgsdir2lem2  16353  konigsberglem5  16938