MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6bbr 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  1851  equsalOLD  1957  necon2abid  2608  eueq3  3053  sbcel12g  3210  sbceqg  3211  sbcnel12g  3212  sbcne12g  3213  n0moeu  3584  reldisj  3615  r19.3rz  3663  r19.3rzv  3665  r19.9rzv  3666  ordelpss  4551  reusv2lem5  4669  ordsucun  4746  dflim3  4768  dfom2  4788  peano5  4809  rabxp  4855  elrng  5003  iss  5130  elimasni  5172  eliniseg  5174  xpcan  5246  xpcan2  5247  fcnvres  5561  dffv3  5665  funimass4  5717  fndmdif  5774  fneqeql  5778  funimass3  5786  elrnrexdmb  5815  dff4  5823  fconst4  5896  elunirnALT  5940  eqfnov  6116  caoftrn  6279  mpt2xopovel  6408  brtpos  6425  rntpos  6429  opiota  6472  f1ocnvfv3  6522  ordgt0ge1  6678  ondif2  6683  oelim2  6775  omabs  6827  iiner  6913  erinxp  6915  qliftfun  6926  ordunifi  7294  elfi2  7355  elfiun  7371  fifo  7373  noinfep  7548  cantnfrescl  7566  cantnf  7583  rankonidlem  7688  r1pwOLD  7706  pr2nelem  7822  cardalephex  7905  alephinit  7910  dfac5lem4  7941  cflim2  8077  cfsmolem  8084  compssiso  8188  fin1a2lem11  8224  itunisuc  8233  axdclem  8333  brdom6disj  8344  alephreg  8391  fpwwe2lem9  8447  pwfseqlem3  8469  pwfseqlem4  8471  indpi  8718  nqereu  8740  ordpinq  8754  ltanq  8782  ltmnq  8783  suplem2pr  8864  map2psrpr  8919  ssxr  9079  letri3  9094  leltne  9098  ltneg  9461  leneg  9464  suprnub  9904  negiso  9917  infmrgelb  9921  elnnnn0  10196  nn0sub  10203  zrevaddcl  10254  znnsub  10255  znn0sub  10256  prime  10283  eluz2  10427  indstr  10478  eluz2b1  10480  qrevaddcl  10529  rpneg  10574  xrleltne  10671  dfle2  10673  dflt2  10674  xrletri3  10678  supxrleub  10838  infmxrgelb  10846  ixxin  10866  iccid  10894  elicopnf  10933  iccsplit  10962  fzsplit2  11009  fzsn  11027  fzpr  11034  uzsplit  11049  injresinj  11128  om2uzf1oi  11221  lt2sqi  11398  le2sqi  11399  hashsdom  11583  hashf1lem1  11632  fz1isolem  11638  ccatlcan  11706  ccatrcan  11707  cnpart  11973  limsuplt  12201  rlimresb  12287  mertenslem2  12590  sadadd2lem2  12890  saddisjlem  12904  bitsuz  12914  gcddiv  12977  algcvgblem  12996  isprm2lem  13014  isprm3  13016  isprm5  13040  prmreclem5  13216  vdwapun  13270  vdwmc2  13275  ramcl  13325  pwsle  13642  ismre  13743  mreacs  13811  acsfn  13812  iscatd2  13834  cidpropd  13864  oppcsect2  13928  isfunc  13989  setcinv  14173  tosso  14393  ipodrsfi  14517  acsfiindd  14531  imasmnd2  14660  submacs  14693  imasgrp2  14861  issubg  14872  subgacs  14903  eqgval  14917  gaorber  15013  isslw  15170  sylow2alem2  15180  sylow2a  15181  sylow3lem6  15194  efgcpbllemb  15315  prmcyg  15431  gsum2d2lem  15475  gsumcom2  15477  subgdmdprd  15520  dprd2d2  15530  pgpfac1lem2  15561  pgpfac1lem4  15564  imasrng  15653  drngmulne0  15785  lssle0  15954  lssacs  15971  lssats2  16004  lvecvsn0  16109  islpir  16248  isnzr2  16262  zndvds  16754  znleval  16759  znleval2  16760  eltg2b  16948  discld  17077  opnssneib  17103  cldlp  17137  restbas  17145  leordtvallem1  17197  leordtvallem2  17198  ssidcn  17242  cnprest2  17277  lmss  17285  perfcls  17352  cmpfi  17394  1stccnp  17447  subislly  17466  hausmapdom  17485  iskgen3  17503  kgencn  17510  ptpjpre1  17525  xkoccn  17573  txrest  17585  txlm  17602  txkgen  17606  xkopt  17609  xkoinjcn  17641  imasnopn  17644  imasncld  17645  imasncls  17646  qtopcn  17668  kqfeq  17678  isr0  17691  fbfinnfr  17795  trfbas  17798  fbunfip  17823  ufileu  17873  cfinufil  17882  fmid  17914  txflf  17960  fclsrest  17978  alexsubALT  18004  tsmsres  18095  ucnima  18233  fmucndlem  18243  bldisj  18330  xmeter  18354  elbl4  18484  metuel2  18486  restmetu  18490  dscopn  18493  bl2ioo  18695  isphtpc  18891  tchcph  19066  lmmbr2  19084  lmmbrf  19087  iscau2  19102  iscauf  19105  caucfil  19108  metcld  19130  metcld2  19131  bcthlem1  19147  bcthlem4  19150  cldcss2  19211  ovolgelb  19244  ovoliunlem1  19266  ismbfcn  19391  mbfmax  19409  mbfimaopnlem  19415  i1faddlem  19453  i1fmullem  19454  i1fres  19465  i1fpos  19466  itg1climres  19474  xrge0f  19491  itgresr  19538  iblcnlem1  19547  limcun  19650  dvres  19666  mdegmullem  19869  ply1remlem  19953  plyremlem  20089  vieta1  20097  ulmcau  20179  sineq0  20297  coseq1  20298  ang180lem3  20521  cubic  20557  atandm  20584  atandm2  20585  atandm3  20586  rlimcnp  20672  rlimcnp2  20673  vmappw  20767  dchrelbas3  20890  dchrelbas4  20895  dchrsum2  20920  bposlem6  20941  dchrisumlem3  21053  pntleml  21173  nbgrael  21305  nb3gra2nb  21331  nbcusgra  21339  trls  21401  istrl2  21403  0pth  21425  0spth  21426  wlkdvspthlem  21456  0crct  21462  0cycl  21463  eupath2lem2  21549  elghom  21800  nmoolb  22121  nmlno0lem  22143  ubthlem1  22221  ocsh  22634  shle0  22793  eigrei  23186  adjeu  23241  nmoplb  23259  nmfnlb  23276  eleigvec2  23310  nmlnop0iALT  23347  cnlnadjlem5  23423  adjbdln  23435  jplem2  23621  cvbr2  23635  mdsl2bi  23675  chrelat3  23723  funcnvmpt  23925  funcnv5mpt  23926  gtiso  23930  xrdifh  23980  fzsplit3  23987  xrge0tsmsbi  24054  unitdivcld  24104  lmxrge0  24142  eldifpr  24189  eldiftp  24190  dstfrvunirn  24512  ballotlemfc0  24530  ballotlemfcc  24531  subfacp1lem3  24648  subfacp1lem5  24650  erdszelem9  24665  kur14  24682  iscvm  24726  dfpo2  25137  fundmpss  25147  dfon2  25173  elpredg  25203  preduz  25225  tfrALTlem  25301  nofulllem1  25381  nofulllem2  25382  dfbigcup2  25464  dffun10  25478  brimg  25501  funpartfv  25509  dfrdg4  25514  brbtwn2  25559  axsegconlem6  25576  axsegcon  25581  ax5seg  25592  axpasch  25595  axeuclid  25617  axcontlem4  25621  cgr3permute3  25696  segletr  25763  segleantisym  25764  seglelin  25765  itg2addnclem  25958  itg2addnc  25960  itgaddnclem2  25965  iblabsnclem  25969  fneval  26059  locfindis  26077  neibastop3  26083  eltail  26095  filnetlem4  26102  caures  26158  heiborlem3  26214  heiborlem10  26221  divrngidl  26330  prtlem10  26406  prtlem16  26410  prtlem19  26419  prtex  26421  prter3  26423  isnacs2  26452  rabrenfdioph  26567  expdiophlem1  26784  pw2f1ocnv  26800  pwfi2f1o  26930  numinfctb  26938  dfacbasgrp  26943  lindsmm  26968  islinds3  26974  islindf4  26978  islnr3  26989  subrgacs  27178  sdrgacs  27179  isdomn3  27193  dvconstbi  27221  rfcnpre3  27373  rfcnpre4  27374  stoweidlem59  27477  vdn1frgrav2  27780  vdgn1frgrav2  27781  sbc3org  27960  trsbc  27969  sbcssOLD  27971  bnj919  28475  bnj976  28487  bnj1542  28567  bnj150  28586  bnj151  28587  bnj607  28626  bnj852  28631  bnj873  28634  bnj938  28647  bnj1171  28708  bnj1388  28741  bnj1489  28764  equsalNEW7  28826  islshpat  29133  lcvbr2  29138  lcvbr3  29139  lshpsmreu  29225  isat3  29423  hlrelat5N  29516  islpln5  29650  cdlemblem  29908  paddvaln0N  29916  paddval0  29925  cdlemefrs29bpre1  30512  cdlemefrs29cpre1  30513  cdlemg27b  30811  cdlemg33c  30823  cdlemg33e  30825  diaglbN  31171  cdlemm10N  31234  dicopelval2  31297  dicelval2N  31298  dihopelvalcpre  31364  dihglbcpreN  31416  dih1dimatlem  31445  dihatexv  31454  dvh4dimlem  31559  mapdpglem3  31791  hdmap14lem13  31999  hdmapglem7a  32046
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