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

Theorem syl6bbr 263
Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
syl6bbr.1
syl6bbr.2
Assertion
Ref Expression
syl6bbr

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2
2 syl6bbr.2 . . 3
32bicomi 202 . 2
41, 3syl6bb 261 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3bitr4g  288  bibi2i  313  mtt  339  nbn2  345  rbaibr  905  3bior1fd  1334  3biant1d  1337  clelab  2601  necon2abidOLD  2712  eueq3  3274  n0moeu  3798  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  sbcne12  3827  sbcne12gOLD  3828  reldisj  3870  raldifeq  3917  r19.3rz  3920  r19.3rzv  3922  r19.9rzv  3923  eldifpr  4046  eldiftp  4072  reusv2lem5  4657  otthg  4735  ordelpss  4911  rabxp  5041  elrng  5199  iss  5326  elimasni  5369  eliniseg  5371  xpcan  5448  xpcan2  5449  fcnvres  5767  dffv3  5867  funimass4  5924  fndmdif  5991  fneqeql  5995  funimass3  6003  elrnrexdmb  6036  dff4  6045  fnsnb  6090  fconst4  6136  elunirn  6163  f12dfv  6179  riota1  6276  riota2df  6278  f1ocnvfv3  6292  eqfnov  6408  elrnmpt2res  6416  caoftrn  6575  ordsucun  6660  dflim3  6682  dfom2  6702  peano5  6723  opiota  6859  suppssr  6950  mpt2xopovel  6967  brtpos  6983  rntpos  6987  ordgt0ge1  7166  ondif2  7171  oelim2  7263  omabs  7315  iiner  7402  erinxp  7404  qliftfun  7415  ordunifi  7790  elfi2  7894  elfiun  7910  fifo  7912  noinfep  8097  cantnflem1  8129  cantnf  8133  cantnfOLD  8155  rankonidlem  8267  r1pwOLD  8285  pr2nelem  8403  cardalephex  8492  alephinit  8497  dfac5lem4  8528  cflim2  8664  cfsmolem  8671  compssiso  8775  fin1a2lem11  8811  itunisuc  8820  axdclem  8920  brdom6disj  8931  alephreg  8978  fpwwe2lem9  9037  pwfseqlem3  9059  pwfseqlem4  9061  indpi  9306  nqereu  9328  ordpinq  9342  ltanq  9370  ltmnq  9371  suplem2pr  9452  map2psrpr  9508  ssxr  9675  letri3  9691  leltne  9695  ltneg  10077  leneg  10080  suprnub  10531  negiso  10544  infmrgelb  10548  elnnnn0  10864  nn0sub  10871  zrevaddcl  10934  znnsub  10935  znn0sub  10936  prime  10968  eluz2  11116  indstr  11179  eluz2b1  11182  qrevaddcl  11233  rpneg  11278  xrleltne  11380  dfle2  11382  dflt2  11383  xrletri3  11387  supxrleub  11547  infmxrgelb  11555  ixxin  11575  iccid  11603  elicopnf  11649  iccsplit  11682  fzsplit2  11739  fzsn  11754  fzpr  11764  uzsplit  11779  injresinj  11926  om2uzf1oi  12064  lt2sqi  12256  le2sqi  12257  hashsdom  12449  hashf1lem1  12504  fz1isolem  12510  ccatlcan  12697  ccatrcan  12698  2swrd2eqwrdeq  12891  cnpart  13073  limsuplt  13302  rlimresb  13388  mertenslem2  13694  fprod2dlem  13784  sadadd2lem2  14100  saddisjlem  14114  bitsuz  14124  gcddiv  14187  algcvgblem  14206  isprm2lem  14224  isprm3  14226  isprm5  14253  prmreclem5  14438  vdwapun  14492  vdwmc2  14497  ramcl  14547  pwsle  14889  ismre  14987  mreacs  15055  acsfn  15056  iscatd2  15078  cidpropd  15105  oppcsect2  15169  isfunc  15233  setcinv  15417  lubeldm  15611  lubval  15614  glbeldm  15624  glbval  15627  tosso  15666  ipodrsfi  15793  acsfiindd  15807  imasmnd2  15957  submacs  15996  imasgrp2  16185  issubg  16201  resgrpisgrp  16222  subgacs  16236  eqgval  16250  gaorber  16346  symgfix2  16441  psgnran  16540  isslw  16628  sylow2alem2  16638  sylow2a  16639  sylow3lem6  16652  efgcpbllemb  16773  prmcyg  16896  gsum2d2lem  17001  gsumcom2  17003  subgdmdprd  17081  dprd2d2  17093  pgpfac1lem2  17126  pgpfac1lem4  17129  imasring  17268  drngmulne0  17418  lssle0  17596  lssacs  17613  lssats2  17646  lvecvsn0  17755  islpir  17897  isnzr2  17911  zndvds  18588  znleval  18593  znleval2  18594  lindsmm  18863  islinds3  18869  islindf4  18873  eltg2b  19460  discld  19590  opnssneib  19616  cldlp  19651  restbas  19659  leordtvallem1  19711  leordtvallem2  19712  ssidcn  19756  cnprest2  19791  lmss  19799  perfcls  19866  cmpfi  19908  1stccnp  19963  subislly  19982  hausmapdom  20001  locfindis  20031  iskgen3  20050  kgencn  20057  ptpjpre1  20072  xkoccn  20120  txrest  20132  txlm  20149  txkgen  20153  xkopt  20156  xkoinjcn  20188  imasnopn  20191  imasncld  20192  imasncls  20193  qtopcn  20215  kqfeq  20225  isr0  20238  fbfinnfr  20342  trfbas  20345  fbunfip  20370  ufileu  20420  cfinufil  20429  fmid  20461  txflf  20507  fclsrest  20525  alexsubALT  20551  tsmsresOLD  20645  tsmsres  20646  ucnima  20784  fmucndlem  20794  bldisj  20901  xmeter  20936  elbl4  21079  restmetu  21090  dscopn  21094  bl2ioo  21297  isphtpc  21494  tchcph  21680  lmmbr2  21698  lmmbrf  21701  iscau2  21716  iscauf  21719  caucfil  21722  metcld  21744  metcld2  21745  bcthlem1  21763  bcthlem4  21766  cldcss2  21857  ovolgelb  21891  ovoliunlem1  21913  ismbfcn  22038  mbfmax  22056  mbfimaopnlem  22062  i1faddlem  22100  i1fmullem  22101  i1fres  22112  i1fpos  22113  itg1climres  22121  xrge0f  22138  itgresr  22185  iblcnlem1  22194  limcun  22299  dvres  22315  mdegmullem  22478  ply1remlem  22563  plyremlem  22700  vieta1  22708  ulmcau  22790  sineq0  22914  coseq1  22915  ang180lem3  23143  cubic  23180  atandm  23207  atandm2  23208  atandm3  23209  rlimcnp  23295  rlimcnp2  23296  vmappw  23390  dchrelbas3  23513  dchrelbas4  23518  dchrsum2  23543  bposlem6  23564  dchrisumlem3  23676  pntleml  23796  lnrot2  24004  islnopp  24113  islmib  24153  brbtwn2  24208  axsegconlem6  24225  axsegcon  24230  ax5seg  24241  axpasch  24244  axeuclid  24266  axcontlem4  24270  usgrac  24351  elusuhgra  24368  nbgrael  24426  nb3gra2nb  24455  nbcusgra  24463  wlkcomp  24525  trls  24538  istrl2  24540  is2wlk  24567  0pth  24572  0spth  24573  wlkdvspthlem  24609  0crct  24626  0cycl  24627  clwlkcomp  24763  clwlkisclwwlklem0  24788  clwlkisclwwlk  24789  el2wlkonotot0  24872  2wot2wont  24886  usg2spthonot1  24890  2spot2iun2spont  24891  isrusgra  24927  isrusgusrgcl  24933  isrusgrac  24935  0eusgraiff0rgracl  24941  rusgranumwlks  24956  eupath2lem2  24978  vdn1frgrav2  25025  vdgn1frgrav2  25026  usgreg2spot  25067  numclwwlkovgel  25088  elghomOLD  25365  nmoolb  25686  nmlno0lem  25708  ubthlem1  25786  ocsh  26201  shle0  26360  eigrei  26753  adjeu  26808  nmoplb  26826  nmfnlb  26843  eleigvec2  26877  nmlnop0iALT  26914  cnlnadjlem5  26990  adjbdln  27002  jplem2  27188  cvbr2  27202  mdsl2bi  27242  chrelat3  27290  disjunsn  27453  ofpreima  27507  funcnvmpt  27510  funcnv5mpt  27511  dfcnv2  27517  gtiso  27519  fpwrelmap  27556  xrdifh  27591  fzsplit3  27599  toslublem  27655  tosglblem  27657  isarchi  27726  xrge0tsmsbi  27776  unitdivcld  27883  lmxrge0  27934  isrrext  27981  issibf  28275  eulerpartlemr  28313  eulerpartlemmf  28314  eulerpartlemn  28320  dstfrvunirn  28413  ballotlemfc0  28431  ballotlemfcc  28432  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem9  28643  kur14  28660  iscvm  28704  mclsax  28929  dfpo2  29184  fundmpss  29196  opelco3  29208  dfon2  29224  elpredg  29258  preduz  29280  nofulllem1  29462  nofulllem2  29463  dfbigcup2  29549  sscoid  29563  funpartfv  29595  dfrdg4  29600  cgr3permute3  29697  segletr  29764  segleantisym  29765  seglelin  29766  cos2h  30046  tan2h  30047  mbfposadd  30062  cnambfre  30063  dvtanlem  30064  itg2addnclem  30066  itg2addnc  30069  iblabsnclem  30078  ftc1anclem1  30090  ftc1anclem5  30094  fneval  30170  neibastop3  30180  eltail  30192  filnetlem4  30199  caures  30253  heiborlem3  30309  heiborlem10  30316  divrngidl  30425  prtlem10  30606  prtlem16  30610  prtlem19  30619  prtex  30621  prter3  30623  isnacs2  30638  rabrenfdioph  30748  expdiophlem1  30963  pw2f1ocnv  30979  pwfi2f1o  31044  numinfctb  31052  dfacbasgrp  31057  islnr3  31064  subrgacs  31149  sdrgacs  31150  isdomn3  31164  hashnzfzclim  31227  dvconstbi  31239  rfcnpre3  31408  rfcnpre4  31409  unima  31441  cncfshift  31676  stoweidlem59  31841  prelpw  32299  uhgrasiz  32394  isfusgracl  32426  isfusgraclALT  32428  fusgraimpclALT2  32431  usgfis  32446  usgfisALT  32450  submgmacs  32492  ismhm0  32493  iscmgmALT  32548  iscsgrpALT  32550  dfiso2  32568  isrnghmmul  32699  sbc3orgOLD  33303  sbcssOLD  33313  bnj919  33825  bnj976  33836  bnj1542  33915  bnj150  33934  bnj151  33935  bnj607  33974  bnj852  33979  bnj873  33982  bnj938  33995  bnj1171  34056  bnj1388  34089  bnj1489  34112  bj-hbntbi  34258  bj-sbceqgALT  34469  islshpat  34742  lcvbr2  34747  lcvbr3  34748  lshpsmreu  34834  isat3  35032  hlrelat5N  35125  islpln5  35259  cdlemblem  35517  paddvaln0N  35525  paddval0  35534  cdlemefrs29bpre1  36123  cdlemefrs29cpre1  36124  cdlemg27b  36422  cdlemg33c  36434  cdlemg33e  36436  diaglbN  36782  cdlemm10N  36845  dicopelval2  36908  dicelval2N  36909  dihopelvalcpre  36975  dihglbcpreN  37027  dih1dimatlem  37056  dihatexv  37065  dvh4dimlem  37170  mapdpglem3  37402  hdmap14lem13  37610  hdmapglem7a  37657  dfhe3  37799
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