MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an23 Unicode version

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
StepHypRef Expression
1 mp3an23.1 . 2  |-  ps
2 mp3an23.2 . . 3  |-  ch
3 mp3an23.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1268 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 653 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  sbciegf  3137  ac6sfi  7289  unfilem1  7309  ordtypelem2  7423  infxpenc2  7838  cda0en  7994  cfsmolem  8085  axdc4lem  8270  1nqenq  8774  mul02lem1  9176  muleqadd  9600  halfcl  10127  rehalfcl  10128  half0  10129  2halves  10130  halfpos2  10131  halfnneg2  10133  halfaddsub  10135  nneo  10287  zeo  10289  peano5uzi  10292  fztp  11036  uzrdgxfr  11235  bcn2  11539  bcpasc  11541  hashxplem  11625  hashfun  11629  swrds2  11809  imre  11842  reim  11843  crim  11849  addcj  11882  imval2  11885  cnpart  11974  sqrlem7  11983  absmax  12062  efgt0  12633  sinf  12654  efi4p  12667  resin4p  12668  recos4p  12669  sinneg  12676  efival  12682  cosadd  12695  sinmul  12702  sinbnd  12710  cosbnd  12711  ef01bndlem  12714  sin01bnd  12715  cos01bnd  12716  sin01gt0  12720  cos01gt0  12721  sin02gt0  12722  rpnnen2lem11  12753  rpnnen2  12754  odd2np1lem  12836  odd2np1  12837  pythagtriplem12  13129  pythagtriplem14  13131  pythagtriplem15  13132  pythagtriplem16  13133  pythagtriplem17  13134  pockthi  13204  prmreclem5  13217  prmreclem6  13218  prmlem0  13357  prdsplusg  13610  prdsmulr  13611  prdsvsca  13612  odinf  15128  lbsexg  16165  mopnex  18441  tngnm  18565  tngngp2  18566  tngngpd  18567  tngngp  18568  addccncf  18819  iihalf1  18829  iihalf2  18831  pjthlem1  19207  ovolunlem1a  19261  ovolunlem1  19262  opnmbllem  19362  vitalilem4  19372  iblcnlem1  19548  itgcnlem  19550  dvmptre  19724  dvmptim  19725  dvlipcn  19747  aaliou3lem3  20130  aaliou3lem8  20131  sincosq1lem  20274  sincosq2sgn  20276  sincosq3sgn  20277  sincosq4sgn  20278  sinq12gt0  20284  abssinper  20295  coskpi  20297  sineq0  20298  coseq1  20299  efeq1  20300  resinf1o  20307  efif1olem2  20314  efif1olem4  20316  logneg2  20379  cxpsqrlem  20462  cxpsqr  20463  logsqr  20464  1cubr  20551  leibpilem1  20649  leibpilem2  20650  basellem3  20734  ppiub  20857  chtublem  20864  chtub  20865  bcmax  20931  bcp1ctr  20932  bposlem2  20938  bposlem6  20942  bposlem9  20945  logdivsum  21096  4ipval2  22054  4ipval3  22058  ipidsq  22059  dipcl  22061  dipcj  22063  ipasslem11  22191  hvmul0  22376  pjhthlem1  22743  h1de2bi  22906  spanunsni  22931  adjeu  23242  nmopge0  23264  nmfnge0  23280  opsqrlem6  23498  mdsl1i  23674  mdsl2bi  23676  mdexchi  23688  superpos  23707  atabsi  23754  dmdbr5ati  23775  cdj3lem1  23787  ofldaddlt  24069  ofldlt1  24071  ofldchr  24072  subfacp1lem2a  24647  subfacp1lem5  24651  subfacp1lem6  24652  subfaclim  24655  sinccvglem  24890  dfon2lem3  25167  dfon2lem7  25171  bpoly2  25819  bpoly3  25820  fsumcube  25822  itg2addnc  25961  ftc1cnnclem  25980  clsun  26024  fdc  26142  constcncf  26161  sub1cncf  26163  sub2cncf  26164  heiborlem7  26219  diophren  26567  psgnghm2  27109  lhe4.4ex1a  27217  sinh-conventional  27830  dp2cl  27860  dpfrac1  27863  atlatmstc  29436
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
  Copyright terms: Public domain W3C validator