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

Theorem syl5bbr 259
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1
syl5bbr.2
Assertion
Ref Expression
syl5bbr

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3
21bicomi 202 . 2
3 syl5bbr.2 . 2
42, 3syl5bb 257 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3bitr3g  287  biass  359  19.16  1957  19.19  1959  sbcom2  2189  sbal2  2205  cbvabOLD  2599  necon1bbid  2707  necon4abidOLD  2709  elabgt  3243  sbceq1a  3338  sbcralt  3408  sbccsbgOLD  3850  sbccsb2  3851  sbccsb2gOLD  3852  disjxun  4450  xp11  5447  ressn  5548  fnssresb  5698  dmfco  5947  dffo4  6047  f1ompt  6053  funressn  6084  fnsuppeq0OLD  6132  elunirnALT  6164  fliftf  6213  resoprab2  6399  elrnmpt2res  6416  ralrnmpt2  6417  iunpw  6614  ordunisuc2  6679  tfis  6689  tfinds  6694  dfom2  6702  fun11iun  6760  opiota  6859  1stconst  6888  2ndconst  6889  fnsuppeq0  6947  iinon  7030  dfsmo2  7037  oeeui  7270  omabs  7315  brecop  7423  ixpsnf1o  7529  boxcutc  7532  ac6sfi  7784  wemapwe  8160  wemapweOLD  8161  sdom2en01  8703  ac6num  8880  zorn2lem7  8903  ttukeylem6  8915  alephval2  8968  fpwwe2  9042  fpwwe  9045  nqereu  9328  suplem2pr  9452  map2psrpr  9508  supsrlem  9509  fimaxre3  10517  infm3  10527  crne0  10554  nn1suc  10582  uzindOLD  10982  xmulneg1  11490  supxrbnd1  11542  supxrbnd2  11543  iccneg  11670  wrdmap  12572  wrdind  12702  cnpart  13073  sqrt00  13097  lo1resb  13387  o1resb  13389  absefib  13933  efieq1re  13934  sadadd2lem2  14100  saddisjlem  14114  prmind2  14228  mreacs  15055  issubc  15204  isfunc  15233  pospo  15603  mrcmndind  15997  eqgval  16250  resscntz  16369  frgpuplem  16790  qusabl  16871  dmdprd  17029  dprdcntz2  17086  dprd2d2  17093  isnzr2  17911  mpfind  18205  gsummoncoe1  18346  pf1ind  18391  chrdvds  18565  chrcong  18566  znleval  18593  isphld  18689  smadiadetr  19177  mp2pm2mplem4  19310  isclo  19588  ist1-2  19848  isnrm2  19859  bwth  19910  bwthOLD  19911  nconsubb  19924  subislly  19982  ptclsg  20116  qtopcld  20214  kqcldsat  20234  qustgplem  20619  tsmssubm  20644  ustuqtop  20749  utop2nei  20753  blval2  21078  caucfil  21722  ioorinv  21985  mbfss  22053  iblss2  22212  dvivthlem1  22409  lhop1  22415  deg1leb  22495  reeff1o  22842  sincosq3sgn  22893  sincosq4sgn  22894  dcubic  23177  efrlim  23299  fsumharmonic  23341  isppw  23388  issqf  23410  fsumdvdsmul  23471  ppiub  23479  lgsdinn0  23615  tglngne  23937  tgelrnln  24010  axlowdimlem14  24258  uhgraop  24304  eupath2lem2  24978  h2hlm  25897  isch2  26141  ch0pss  26363  nmcfnlbi  26971  jplem1  27187  hatomistici  27281  mdsymlem5  27326  cdjreui  27351  reuxfr4d  27389  dfimafnf  27473  funcnvmpt  27510  fpwrelmap  27556  nn0min  27611  isarchi  27726  ordtconlem1  27906  esumfsup  28076  esumpcvgval  28084  measvuni  28185  aean  28216  eulerpartlemgh  28317  ballotlemsima  28454  sgn3da  28480  subfacp1lem2a  28624  subfacp1lem6  28629  ghomf1olem  29034  rtrclreclem.trans  29069  dfres3  29188  eldm3  29191  onsuct0  29906  ptrest  30048  sdclem2  30235  fdc  30238  fdc1  30239  istotbnd3  30267  sstotbnd  30271  prdstotbnd  30290  rrncmslem  30328  diophin  30706  diophun  30707  diophrex  30709  3rexfrabdioph  30730  6rexfrabdioph  30732  7rexfrabdioph  30733  zindbi  30882  isprm7  31192  hashnzfzclim  31227  fveqsb  31362  cncfiooicclem1  31696  stoweidlem35  31817  tz6.12-afv  32258  ndmaovg  32269  isfusgracl  32426  isfusgraclALT  32428  usgfis  32446  usgfisALT  32450  aacllem  33216  bnj1468  33904  lub0N  34914  glb0N  34918  cdlemefrs29bpre0  36122  dvhb1dimN  36712  dvhopellsm  36844  dibord  36886  dochnel2  37119  mapdvalc  37356  mapdval4N  37359
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