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

Theorem mp3an23 1316
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an23.1
mp3an23.2
mp3an23.3
Assertion
Ref Expression
mp3an23

Proof of Theorem mp3an23
StepHypRef Expression
1 mp3an23.1 . 2
2 mp3an23.2 . . 3
3 mp3an23.3 . . 3
42, 3mp3an3 1313 . 2
51, 4mpan2 671 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  sbciegf  3359  ac6sfi  7784  unfilem1  7804  ordtypelem2  7965  infxpenc2  8420  infxpenc2OLD  8424  cda0en  8580  cfsmolem  8671  axdc4lem  8856  1nqenq  9361  mul02lem1  9777  muleqadd  10218  halfcl  10789  rehalfcl  10790  half0  10791  2halves  10792  halfpos2  10793  halfnneg2  10795  halfaddsub  10797  nneo  10971  zeo  10973  peano5uzi  10976  fztp  11765  uzrdgxfr  12077  bcn2  12397  bcpasc  12399  hashxplem  12491  hashfun  12495  swrds2  12883  repsw2  12888  repsw3  12889  imre  12941  reim  12942  crim  12948  addcj  12981  imval2  12984  cnpart  13073  sqrlem7  13082  absmax  13162  efgt0  13838  sinf  13859  efi4p  13872  resin4p  13873  recos4p  13874  sinneg  13881  efival  13887  cosadd  13900  sinmul  13907  sinbnd  13915  cosbnd  13916  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  rpnnen2lem11  13958  rpnnen2  13959  odd2np1lem  14045  odd2np1  14046  pythagtriplem12  14350  pythagtriplem14  14352  pythagtriplem15  14353  pythagtriplem16  14354  pythagtriplem17  14355  pockthi  14425  prmreclem5  14438  prmreclem6  14439  prmlem0  14591  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  odinf  16585  lbsexg  17810  psgnghm2  18617  mopnex  21022  tngnm  21165  tngngp2  21166  tngngpd  21167  tngngp  21168  addccncf  21420  iihalf1  21431  iihalf2  21433  pjthlem1  21852  ovolunlem1a  21907  ovolunlem1  21908  opnmbllem  22010  vitalilem4  22020  iblcnlem1  22194  itgcnlem  22196  dvmptre  22372  dvmptim  22373  dvlipcn  22395  mdegldg  22466  aaliou3lem3  22740  aaliou3lem8  22741  sincosq1lem  22890  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  sinq12gt0  22900  abssinper  22911  coskpi  22913  sineq0  22914  coseq1  22915  efeq1  22916  resinf1o  22923  efif1olem2  22930  efif1olem4  22932  logneg2  23000  cxpsqrtlem  23083  cxpsqrt  23084  logsqrt  23085  1cubr  23173  leibpilem1  23271  leibpilem2  23272  basellem3  23356  ppiub  23479  chtublem  23486  chtub  23487  bcmax  23553  bcp1ctr  23554  bposlem2  23560  bposlem6  23564  bposlem9  23567  logdivsum  23718  4ipval2  25618  4ipval3  25622  ipidsq  25623  dipcl  25625  dipcj  25627  ipasslem11  25755  hvmul0  25941  pjhthlem1  26309  h1de2bi  26472  spanunsni  26497  adjeu  26808  nmopge0  26830  nmfnge0  26846  opsqrlem6  27064  mdsl1i  27240  mdsl2bi  27242  mdexchi  27254  superpos  27273  atabsi  27320  dmdbr5ati  27341  cdj3lem1  27353  fpwrelmapffslem  27555  ogrpaddlt  27708  ofldlt1  27803  ofldchr  27804  oddpwdc  28293  eulerpartgbij  28311  subfacp1lem2a  28624  subfacp1lem5  28628  subfacp1lem6  28629  subfaclim  28632  sinccvglem  29038  binomfallfaclem2  29162  dfon2lem3  29217  dfon2lem7  29221  predeq1  29246  wrecseq1  29339  wsuceq1  29371  bpoly2  29819  bpoly3  29820  fsumcube  29822  sin2h  30045  cos2h  30046  tan2h  30047  opnmbllem0  30050  mblfinlem3  30053  dvtanlem  30064  itg2addnclem3  30068  ftc1cnnclem  30088  ftc1anclem6  30095  ftc2nc  30099  dvasin  30103  clsun  30146  fdc  30238  constcncf  30255  sub1cncf  30257  sub2cncf  30258  heiborlem7  30313  diophren  30747  lhe4.4ex1a  31234  dirkerper  31878  zlmodzxznm  33098  sinh-conventional  33133  dp2cl  33163  dpfrac1  33166  atlatmstc  35044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator