Theorem mp3an23 1271

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an23	|- ( ph -> th )

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1268	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 653	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  sbciegf  3152  ac6sfi  7310  unfilem1  7330  ordtypelem2  7444  infxpenc2  7859  cda0en  8015  cfsmolem  8106  axdc4lem  8291  1nqenq  8795  mul02lem1  9198  muleqadd  9622  halfcl  10149  rehalfcl  10150  half0  10151  2halves  10152  halfpos2  10153  halfnneg2  10155  halfaddsub  10157  nneo  10309  zeo  10311  peano5uzi  10314  fztp  11058  uzrdgxfr  11261  bcn2  11565  bcpasc  11567  hashxplem  11651  hashfun  11655  swrds2  11835  imre  11868  reim  11869  crim  11875  addcj  11908  imval2  11911  cnpart  12000  sqrlem7  12009  absmax  12088  efgt0  12659  sinf  12680  efi4p  12693  resin4p  12694  recos4p  12695  sinneg  12702  efival  12708  cosadd  12721  sinmul  12728  sinbnd  12736  cosbnd  12737  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  rpnnen2lem11  12779  rpnnen2  12780  odd2np1lem  12862  odd2np1  12863  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem15  13158  pythagtriplem16  13159  pythagtriplem17  13160  pockthi  13230  prmreclem5  13243  prmreclem6  13244  prmlem0  13383  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  odinf  15154  lbsexg  16191  mopnex  18502  tngnm  18645  tngngp2  18646  tngngpd  18647  tngngp  18648  addccncf  18899  iihalf1  18909  iihalf2  18911  pjthlem1  19291  ovolunlem1a  19345  ovolunlem1  19346  opnmbllem  19446  vitalilem4  19456  iblcnlem1  19632  itgcnlem  19634  dvmptre  19808  dvmptim  19809  dvlipcn  19831  aaliou3lem3  20214  aaliou3lem8  20215  sincosq1lem  20358  sincosq2sgn  20360  sincosq3sgn  20361  sincosq4sgn  20362  sinq12gt0  20368  abssinper  20379  coskpi  20381  sineq0  20382  coseq1  20383  efeq1  20384  resinf1o  20391  efif1olem2  20398  efif1olem4  20400  logneg2  20463  cxpsqrlem  20546  cxpsqr  20547  logsqr  20548  1cubr  20635  leibpilem1  20733  leibpilem2  20734  basellem3  20818  ppiub  20941  chtublem  20948  chtub  20949  bcmax  21015  bcp1ctr  21016  bposlem2  21022  bposlem6  21026  bposlem9  21029  logdivsum  21180  4ipval2  22157  4ipval3  22161  ipidsq  22162  dipcl  22164  dipcj  22166  ipasslem11  22294  hvmul0  22479  pjhthlem1  22846  h1de2bi  23009  spanunsni  23034  adjeu  23345  nmopge0  23367  nmfnge0  23383  opsqrlem6  23601  mdsl1i  23777  mdsl2bi  23779  mdexchi  23791  superpos  23810  atabsi  23857  dmdbr5ati  23878  cdj3lem1  23890  ofldaddlt  24194  ofldlt1  24196  ofldchr  24197  subfacp1lem2a  24819  subfacp1lem5  24823  subfacp1lem6  24824  subfaclim  24827  sinccvglem  25062  binomfallfaclem2  25307  dfon2lem3  25355  dfon2lem7  25359  bpoly2  26007  bpoly3  26008  fsumcube  26010  mblfinlem  26143  mblfinlem2  26144  itg2addnclem3  26157  ftc1cnnclem  26177  clsun  26221  fdc  26339  constcncf  26358  sub1cncf  26360  sub2cncf  26361  heiborlem7  26416  diophren  26764  psgnghm2  27306  lhe4.4ex1a  27414  sinh-conventional  28196  dp2cl  28226  dpfrac1  28229  atlatmstc  29802

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938