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

Theorem syl6rbbr 264
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1
syl6rbbr.2
Assertion
Ref Expression
syl6rbbr

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2
2 syl6rbbr.2 . . 3
32bicomi 202 . 2
41, 3syl6rbb 262 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  baib  903  necon2abid  2711  reu8  3295  sbc6g  3353  r19.28z  3921  r19.28zv  3924  r19.37zv  3925  r19.45zv  3926  r19.44zv  3927  r19.27z  3928  r19.27zv  3929  r19.36zv  3930  ralidm  3933  ralsnsg  4061  rexsnsOLD  4063  eldifvsn  4162  ssunsn2  4189  iunconst  4339  iinconst  4340  reusv7OLD  4664  ordsseleq  4912  funssres  5633  fncnv  5657  fresaun  5761  dff1o5  5830  funimass4  5924  fndmdifeq0  5993  fneqeql2  5996  unpreima  6013  dffo3  6046  fnnfpeq0  6102  funfvima  6147  f1eqcocnv  6204  fliftf  6213  isocnv3  6228  isomin  6233  eloprabga  6389  mpt22eqb  6411  elpwun  6613  dfom2  6702  opabex3d  6778  opabex3  6779  f1oweALT  6784  fnwelem  6915  mptsuppd  6942  oe0m1  7190  oarec  7230  boxcutc  7532  ordunifi  7790  r1fin  8212  rankr1c  8260  iscard  8377  iscard2  8378  cardval2  8393  dfac3  8523  kmlem8  8558  infinf  8962  xrlenlt  9673  ltxrlt  9676  negcon2  9895  mulne0b  10215  dfinfmr  10545  crne0  10554  elznn  10905  zmax  11208  zq  11217  elfznelfzo  11915  hashneq0  12434  sqrtneglem  13100  rexfiuz  13180  rexanuz2  13182  sumsplit  13583  fsum2dlem  13585  fsumcom2  13589  fprodcom2  13788  odd2np1  14046  divalgb  14062  gcdcllem2  14150  mrcidb2  15015  lbsacsbs  17802  islpir2  17899  domnmuln0  17947  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  islinds2  18848  islbs4  18867  mamucl  18903  mavmulcl  19049  mdetunilem8  19121  iscld4  19566  iscon2  19915  kgencn  20057  tx1cn  20110  tx2cn  20111  elmptrab  20328  isfbas  20330  fbfinnfr  20342  cnfcf  20543  fmucndlem  20794  prdsxmslem2  21032  blval2  21078  cnbl0  21281  cnblcld  21282  metcld  21744  ismbf  22037  ismbfcn  22038  itg1val2  22091  itg2split  22156  itg2monolem1  22157  aannenlem1  22724  pilem1  22846  sinq34lt0t  22902  ellogrn  22947  logeftb  22968  ercgrg  23908  isusgra0  24347  usgraop  24350  constr3lem2  24646  ch0pss  26363  h1de2ctlem  26473  adjsym  26752  eigposi  26755  dfadj2  26804  elnlfn  26847  xppreima  27487  1stpreima  27524  2ndpreima  27525  qtophaus  27839  prsdm  27896  prsrn  27897  1stmbfm  28231  2ndmbfm  28232  eulerpartlemn  28320  nofulllem1  29462  dffun10  29564  hfext  29840  cnambfre  30063  isfne4b  30159  neifg  30189  0totbnd  30269  isnacs2  30638  mrefg3  30640  pw2f1ocnv  30979  acsfn1p  31148  climreeq  31619  funressnfv  32213  fncnvimaeqv  32626  sbcoreleleq  33306  bnj1454  33900  bnj984  34010  cvrval2  34999  cvrnbtwn2  35000  cvrnbtwn4  35004  hlateq  35123  islpln5  35259  islvol5  35303  pmap11  35486  4atex  35800  cdleme0ex2N  35949  cdlemefrs29pre00  36121  diaord  36774  dihmeetlem13N  37046  lcfl1  37219  lcfls1N  37262  mapdpglem3  37402  taupilem3  37694  xpcogend  37773
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