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

Theorem sylnibr 305
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnibr.1
sylnibr.2
Assertion
Ref Expression
sylnibr

Proof of Theorem sylnibr
StepHypRef Expression
1 sylnibr.1 . 2
2 sylnibr.2 . . 3
32bicomi 202 . 2
41, 3sylnib 304 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  otiunsndisj  4758  pofun  4821  disjen  7694  php3  7723  sdom1  7739  wemappo  7995  cnfcom2lem  8166  cnfcom2lemOLD  8174  zfregs2  8185  cfsuc  8658  fin1a2lem12  8812  ac6num  8880  canth4  9046  pwfseqlem3  9059  gchpwdom  9069  gchaleph  9070  gchhar  9078  difreicc  11681  fzpreddisj  11758  lsw0  12586  fprodntriv  13749  prmreclem5  14438  ramcl2lem  14527  cidpropd  15105  gsumpropd2lem  15900  isnsgrp  15915  isnmnd  15924  odinf  16585  frgpnabllem1  16877  ablfac1lem  17119  frlmssuvc2  18826  frlmssuvc2OLD  18828  lmmo  19881  xkohaus  20154  snfil  20365  supfil  20396  hauspwpwf1  20488  tsmsfbas  20626  reconnlem2  21332  minveclem3b  21843  dvply1  22680  taylthlem2  22769  wilthlem2  23343  lgseisenlem1  23624  axlowdimlem6  24250  isusgra0  24347  usgraop  24350  usgra2edg1  24383  nbgra0edg  24432  cusgrares  24472  uvtx01vtx  24492  spthispth  24575  4cycl2vnunb  25017  frgrawopreglem4  25047  2spotdisj  25061  2spotiundisj  25062  xrge0infss  27580  qqhf  27967  signstfvneq0  28529  subfacp1lem1  28623  pocnv  29193  wsuclem  29381  wsuclb  29384  nofulllem5  29466  filnetlem4  30199  heibor1lem  30305  notornotel2  30496  jm2.23  30938  rpnnen3lem  30973  fnwe2lem2  30997  lcmgcdlem  31212  jcn  31427  fzdifsuc2  31512  icoiccdif  31564  fprodn0f  31594  climrec  31609  sumnnodd  31636  lptioo2  31637  lptioo1  31638  limcresiooub  31648  limcresioolb  31649  icccncfext  31690  cncfiooicclem1  31696  dvmptfprodlem  31741  stoweidlem34  31816  stoweidlem39  31821  stoweidlem59  31841  stirlinglem8  31863  dirkercncflem2  31886  fourierdlem12  31901  fourierdlem40  31929  fourierdlem42  31931  fourierdlem48  31937  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  elaa2  32017  etransc  32066  otiunsndisjX  32301  usg2edgneu  32412  0nodd  32498  cznnring  32764  bnj1417  34097  bj-abfal  34474  pmap0  35489  mapdh6eN  37467  mapdh7dN  37477  hdmap1l6e  37542
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
  Copyright terms: Public domain W3C validator