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

Theorem syl6bbr 255
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6bbr  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6bbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 194 . 2  |-  ( ch  <->  th )
41, 3syl6bb 253 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitr4g  280  bibi2i  305  mtt  330  nbn2  335  3bior1fd  1289  3biant1d  1292  equsalhwOLD  1861  equsalOLD  2000  necon2abid  2655  eueq3  3101  sbcel12g  3258  sbceqg  3259  sbcnel12g  3260  sbcne12g  3261  n0moeu  3632  reldisj  3663  r19.3rz  3711  r19.3rzv  3713  r19.9rzv  3714  ordelpss  4601  reusv2lem5  4720  ordsucun  4797  dflim3  4819  dfom2  4839  peano5  4860  rabxp  4906  elrng  5054  iss  5181  elimasni  5223  eliniseg  5225  xpcan  5297  xpcan2  5298  fcnvres  5612  dffv3  5716  funimass4  5769  fndmdif  5826  fneqeql  5830  funimass3  5838  elrnrexdmb  5867  dff4  5875  fconst4  5948  elunirnALT  5992  eqfnov  6168  caoftrn  6331  mpt2xopovel  6463  brtpos  6480  rntpos  6484  opiota  6527  f1ocnvfv3  6577  ordgt0ge1  6733  ondif2  6738  oelim2  6830  omabs  6882  iiner  6968  erinxp  6970  qliftfun  6981  ordunifi  7349  elfi2  7411  elfiun  7427  fifo  7429  noinfep  7606  cantnfrescl  7624  cantnf  7641  rankonidlem  7746  r1pwOLD  7764  pr2nelem  7880  cardalephex  7963  alephinit  7968  dfac5lem4  7999  cflim2  8135  cfsmolem  8142  compssiso  8246  fin1a2lem11  8282  itunisuc  8291  axdclem  8391  brdom6disj  8402  alephreg  8449  fpwwe2lem9  8505  pwfseqlem3  8527  pwfseqlem4  8529  indpi  8776  nqereu  8798  ordpinq  8812  ltanq  8840  ltmnq  8841  suplem2pr  8922  map2psrpr  8977  ssxr  9137  letri3  9152  leltne  9156  ltneg  9520  leneg  9523  suprnub  9963  negiso  9976  infmrgelb  9980  elnnnn0  10255  nn0sub  10262  zrevaddcl  10313  znnsub  10314  znn0sub  10315  prime  10342  eluz2  10486  indstr  10537  eluz2b1  10539  qrevaddcl  10588  rpneg  10633  xrleltne  10730  dfle2  10732  dflt2  10733  xrletri3  10737  supxrleub  10897  infmxrgelb  10905  ixxin  10925  iccid  10953  elicopnf  10992  iccsplit  11021  fzsplit2  11068  fzsn  11086  fzpr  11093  uzsplit  11110  injresinj  11192  om2uzf1oi  11285  lt2sqi  11462  le2sqi  11463  hashsdom  11647  hashf1lem1  11696  fz1isolem  11702  ccatlcan  11770  ccatrcan  11771  cnpart  12037  limsuplt  12265  rlimresb  12351  mertenslem2  12654  sadadd2lem2  12954  saddisjlem  12968  bitsuz  12978  gcddiv  13041  algcvgblem  13060  isprm2lem  13078  isprm3  13080  isprm5  13104  prmreclem5  13280  vdwapun  13334  vdwmc2  13339  ramcl  13389  pwsle  13706  ismre  13807  mreacs  13875  acsfn  13876  iscatd2  13898  cidpropd  13928  oppcsect2  13992  isfunc  14053  setcinv  14237  tosso  14457  ipodrsfi  14581  acsfiindd  14595  imasmnd2  14724  submacs  14757  imasgrp2  14925  issubg  14936  subgacs  14967  eqgval  14981  gaorber  15077  isslw  15234  sylow2alem2  15244  sylow2a  15245  sylow3lem6  15258  efgcpbllemb  15379  prmcyg  15495  gsum2d2lem  15539  gsumcom2  15541  subgdmdprd  15584  dprd2d2  15594  pgpfac1lem2  15625  pgpfac1lem4  15628  imasrng  15717  drngmulne0  15849  lssle0  16018  lssacs  16035  lssats2  16068  lvecvsn0  16173  islpir  16312  isnzr2  16326  zndvds  16822  znleval  16827  znleval2  16828  eltg2b  17016  discld  17145  opnssneib  17171  cldlp  17206  restbas  17214  leordtvallem1  17266  leordtvallem2  17267  ssidcn  17311  cnprest2  17346  lmss  17354  perfcls  17421  cmpfi  17463  1stccnp  17517  subislly  17536  hausmapdom  17555  iskgen3  17573  kgencn  17580  ptpjpre1  17595  xkoccn  17643  txrest  17655  txlm  17672  txkgen  17676  xkopt  17679  xkoinjcn  17711  imasnopn  17714  imasncld  17715  imasncls  17716  qtopcn  17738  kqfeq  17748  isr0  17761  fbfinnfr  17865  trfbas  17868  fbunfip  17893  ufileu  17943  cfinufil  17952  fmid  17984  txflf  18030  fclsrest  18048  alexsubALT  18074  tsmsres  18165  ucnima  18303  fmucndlem  18313  bldisj  18420  xmeter  18455  elbl4  18598  metuel2  18601  restmetu  18609  dscopn  18613  bl2ioo  18815  isphtpc  19011  tchcph  19186  lmmbr2  19204  lmmbrf  19207  iscau2  19222  iscauf  19225  caucfil  19228  metcld  19250  metcld2  19251  bcthlem1  19269  bcthlem4  19272  cldcss2  19335  ovolgelb  19368  ovoliunlem1  19390  ismbfcn  19515  mbfmax  19533  mbfimaopnlem  19539  i1faddlem  19577  i1fmullem  19578  i1fres  19589  i1fpos  19590  itg1climres  19598  xrge0f  19615  itgresr  19662  iblcnlem1  19671  limcun  19774  dvres  19790  mdegmullem  19993  ply1remlem  20077  plyremlem  20213  vieta1  20221  ulmcau  20303  sineq0  20421  coseq1  20422  ang180lem3  20645  cubic  20681  atandm  20708  atandm2  20709  atandm3  20710  rlimcnp  20796  rlimcnp2  20797  vmappw  20891  dchrelbas3  21014  dchrelbas4  21019  dchrsum2  21044  bposlem6  21065  dchrisumlem3  21177  pntleml  21297  nbgrael  21430  nb3gra2nb  21456  nbcusgra  21464  trls  21528  istrl2  21530  is2wlk  21557  0pth  21562  0spth  21563  wlkdvspthlem  21599  0crct  21605  0cycl  21606  eupath2lem2  21692  elghom  21943  nmoolb  22264  nmlno0lem  22286  ubthlem1  22364  ocsh  22777  shle0  22936  eigrei  23329  adjeu  23384  nmoplb  23402  nmfnlb  23419  eleigvec2  23453  nmlnop0iALT  23490  cnlnadjlem5  23566  adjbdln  23578  jplem2  23764  cvbr2  23778  mdsl2bi  23818  chrelat3  23866  ofpreima  24073  funcnvmpt  24075  funcnv5mpt  24076  gtiso  24080  xrdifh  24135  fzsplit3  24142  toslub  24183  tosglb  24184  xrge0tsmsbi  24216  isarchi  24244  unitdivcld  24291  lmxrge0  24329  eldifpr  24384  eldiftp  24385  issibf  24640  dstfrvunirn  24724  ballotlemfc0  24742  ballotlemfcc  24743  subfacp1lem3  24860  subfacp1lem5  24862  erdszelem9  24877  kur14  24894  iscvm  24938  dfpo2  25370  fundmpss  25382  opelco3  25395  dfon2  25411  elpredg  25445  preduz  25467  nofulllem1  25649  nofulllem2  25650  dfbigcup2  25736  sscoid  25750  funpartfv  25782  dfrdg4  25787  brbtwn2  25836  axsegconlem6  25853  axsegcon  25858  ax5seg  25869  axpasch  25872  axeuclid  25894  axcontlem4  25898  cgr3permute3  25973  segletr  26040  segleantisym  26041  seglelin  26042  mbfposadd  26244  cnambfre  26245  itg2addnclem  26246  itg2addnc  26249  iblabsnclem  26258  fneval  26348  locfindis  26366  neibastop3  26372  eltail  26384  filnetlem4  26391  caures  26447  heiborlem3  26503  heiborlem10  26510  divrngidl  26619  prtlem10  26695  prtlem16  26699  prtlem19  26708  prtex  26710  prter3  26712  isnacs2  26741  rabrenfdioph  26856  expdiophlem1  27073  pw2f1ocnv  27089  pwfi2f1o  27218  numinfctb  27226  dfacbasgrp  27231  lindsmm  27256  islinds3  27262  islindf4  27266  islnr3  27277  subrgacs  27466  sdrgacs  27467  isdomn3  27481  dvconstbi  27509  rfcnpre3  27661  rfcnpre4  27662  stoweidlem59  27765  otthg  28044  f12dfv  28056  el2wlkonotot0  28282  2wot2wont  28296  usg2spthonot1  28300  2spot2iun2spont  28301  vdn1frgrav2  28343  vdgn1frgrav2  28344  usgreg2spot  28383  sbc3org  28543  trsbc  28552  sbcssOLD  28554  bnj919  29063  bnj976  29075  bnj1542  29155  bnj150  29174  bnj151  29175  bnj607  29214  bnj852  29219  bnj873  29222  bnj938  29235  bnj1171  29296  bnj1388  29329  bnj1489  29352  equsalNEW7  29414  ax7w14lemAUX7  29596  islshpat  29742  lcvbr2  29747  lcvbr3  29748  lshpsmreu  29834  isat3  30032  hlrelat5N  30125  islpln5  30259  cdlemblem  30517  paddvaln0N  30525  paddval0  30534  cdlemefrs29bpre1  31121  cdlemefrs29cpre1  31122  cdlemg27b  31420  cdlemg33c  31432  cdlemg33e  31434  diaglbN  31780  cdlemm10N  31843  dicopelval2  31906  dicelval2N  31907  dihopelvalcpre  31973  dihglbcpreN  32025  dih1dimatlem  32054  dihatexv  32063  dvh4dimlem  32168  mapdpglem3  32400  hdmap14lem13  32608  hdmapglem7a  32655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator