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

Theorem syl6bbr 254
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 193 . 2  |-  ( ch  <->  th )
41, 3syl6bb 252 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr4g  279  bibi2i  304  mtt  329  nbn2  334  equsalhw  1742  equsal  1913  necon2abid  2516  eueq3  2953  sbcabel  3081  sbcel12g  3109  sbceqg  3110  sbcnel12g  3111  sbcne12g  3112  n0moeu  3480  reldisj  3511  r19.3rz  3558  r19.3rzv  3560  r19.9rzv  3561  ordelpss  4436  reusv2lem5  4555  ordsucun  4632  dflim3  4654  dfom2  4674  peano5  4695  rabxp  4741  elrng  4887  iss  5014  elimasni  5056  eliniseg  5058  xpcan  5128  xpcan2  5129  fcnvres  5434  dffv3  5537  funimass4  5589  fndmdif  5645  fneqeql  5649  funimass3  5657  dff4  5690  fconst4  5752  elunirnALT  5795  eqfnov  5966  caoftrn  6128  brtpos  6259  rntpos  6263  opiota  6306  f1ocnvfv3  6356  ordgt0ge1  6512  ondif2  6517  oelim2  6609  omabs  6661  iiner  6747  erinxp  6749  qliftfun  6759  ordunifi  7123  elfi2  7184  elfiun  7199  fifo  7201  noinfep  7376  cantnfrescl  7394  cantnf  7411  rankonidlem  7516  r1pwOLD  7534  pr2nelem  7650  cardalephex  7733  alephinit  7738  dfac5lem4  7769  cflim2  7905  cfsmolem  7912  compssiso  8016  fin1a2lem11  8052  itunisuc  8061  axdclem  8162  brdom6disj  8173  alephreg  8220  fpwwe2lem9  8276  pwfseqlem3  8298  pwfseqlem4  8300  indpi  8547  nqereu  8569  ordpinq  8583  ltanq  8611  ltmnq  8612  suplem2pr  8693  map2psrpr  8748  ssxr  8908  letri3  8923  leltne  8927  ltneg  9290  leneg  9293  suprnub  9733  negiso  9746  infmrgelb  9750  elnnnn0  10023  nn0sub  10030  zrevaddcl  10079  znnsub  10080  znn0sub  10081  prime  10108  eluz2  10252  indstr  10303  eluz2b1  10305  qrevaddcl  10354  rpneg  10399  xrleltne  10495  dfle2  10497  dflt2  10498  xrletri3  10502  supxrleub  10661  infmxrgelb  10669  ixxin  10689  iccid  10717  elicopnf  10755  iccsplit  10784  fzsplit2  10831  fzsn  10849  fzpr  10856  uzsplit  10871  om2uzf1oi  11032  lt2sqi  11208  le2sqi  11209  hashsdom  11379  hashf1lem1  11409  fz1isolem  11415  ccatlcan  11480  ccatrcan  11481  cnpart  11741  limsuplt  11969  rlimresb  12055  mertenslem2  12357  sadadd2lem2  12657  saddisjlem  12671  bitsuz  12681  gcddiv  12744  algcvgblem  12763  isprm2lem  12781  isprm3  12783  isprm5  12807  prmreclem5  12983  vdwapun  13037  vdwmc2  13042  ramcl  13092  pwsle  13407  ismre  13508  mreacs  13576  acsfn  13577  iscatd2  13599  cidpropd  13629  oppcsect2  13693  isfunc  13754  setcinv  13938  tosso  14158  ipodrsfi  14282  acsfiindd  14296  imasmnd2  14425  submacs  14458  imasgrp2  14626  issubg  14637  subgacs  14668  eqgval  14682  gaorber  14778  isslw  14935  sylow2alem2  14945  sylow2a  14946  sylow3lem6  14959  efgcpbllemb  15080  prmcyg  15196  gsum2d2lem  15240  gsumcom2  15242  subgdmdprd  15285  dprd2d2  15295  pgpfac1lem2  15326  pgpfac1lem4  15329  imasrng  15418  drngmulne0  15550  lssle0  15723  lssacs  15740  lssats2  15773  lvecvsn0  15878  islpir  16017  isnzr2  16031  zndvds  16519  znleval  16524  znleval2  16525  eltg2b  16713  discld  16842  opnssneib  16868  cldlp  16897  restbas  16905  leordtvallem1  16956  leordtvallem2  16957  ssidcn  17001  cnprest2  17034  lmss  17042  perfcls  17109  cmpfi  17151  1stccnp  17204  subislly  17223  hausmapdom  17242  iskgen3  17260  kgencn  17267  ptpjpre1  17282  xkoccn  17329  txrest  17341  txlm  17358  txkgen  17362  xkopt  17365  xkoinjcn  17397  qtopcn  17421  kqfeq  17431  isr0  17444  fbfinnfr  17552  trfbas  17555  fbunfip  17580  ufileu  17630  cfinufil  17639  fmid  17671  txflf  17717  fclsrest  17735  alexsubALT  17761  tsmsres  17842  bldisj  17971  xmeter  17995  dscopn  18112  bl2ioo  18314  isphtpc  18508  tchcph  18683  lmmbr2  18701  lmmbrf  18704  iscau2  18719  iscauf  18722  caucfil  18725  metcld  18747  metcld2  18748  bcthlem1  18762  bcthlem4  18765  cldcss2  18822  ovolgelb  18855  ovoliunlem1  18877  ismbfcn  19002  mbfmax  19020  mbfimaopnlem  19026  i1faddlem  19064  i1fmullem  19065  i1fres  19076  i1fpos  19077  itg1climres  19085  xrge0f  19102  itgresr  19149  iblcnlem1  19158  limcun  19261  dvres  19277  itgsubst  19412  mdegmullem  19480  ply1remlem  19564  plyremlem  19700  vieta1  19708  ulmcau  19788  sineq0  19905  coseq1  19906  ang180lem3  20125  cubic  20161  atandm  20188  atandm2  20189  atandm3  20190  rlimcnp  20276  rlimcnp2  20277  vmappw  20370  dchrelbas3  20493  dchrelbas4  20498  dchrsum2  20523  bposlem6  20544  dchrisumlem3  20656  pntleml  20776  elghom  21046  nmoolb  21365  nmlno0lem  21387  ubthlem1  21465  ocsh  21878  shle0  22037  eigrei  22430  adjeu  22485  nmoplb  22503  nmfnlb  22520  eleigvec2  22554  nmlnop0iALT  22591  cnlnadjlem5  22667  adjbdln  22679  jplem2  22865  cvbr2  22879  mdsl2bi  22919  chrelat3  22967  fzsplit3  23047  ballotlemfc0  23067  ballotlemfcc  23068  ofrn2  23222  funcnvmpt  23250  funcnv5mpt  23251  gtiso  23256  xrdifh  23288  unitdivcld  23300  lmxrge0  23390  xrge0tsmsbi  23398  eldifpr  23409  eldiftp  23410  dstfrvunirn  23690  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem9  23745  kur14  23762  iscvm  23805  eupath2lem2  23917  dfpo2  24183  fundmpss  24193  dfon2  24219  elpredg  24249  preduz  24271  tfrALTlem  24347  nofulllem1  24427  nofulllem2  24428  dfbigcup2  24510  dffun10  24524  brimg  24547  funpartfv  24555  dfrdg4  24560  brbtwn2  24605  axsegconlem6  24622  axsegcon  24627  ax5seg  24638  axpasch  24641  axeuclid  24663  axcontlem4  24667  cgr3permute3  24742  segletr  24809  segleantisym  24810  seglelin  24811  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itgaddnclem2  25010  iblabsnclem  25014  splint  25151  inttpemp  25242  iint  25715  algi  25830  rdmob  25851  vtarsuelt  25998  pdiveql  26271  abhp2  26278  bhp2a  26279  fneval  26390  locfindis  26408  neibastop3  26414  eltail  26426  filnetlem4  26433  caures  26579  heiborlem3  26640  heiborlem10  26647  divrngidl  26756  prtlem10  26836  prtlem16  26840  prtlem19  26849  prtex  26851  prter3  26853  isnacs2  26884  rabrenfdioph  27000  expdiophlem1  27217  pw2f1ocnv  27233  pwfi2f1o  27363  numinfctb  27371  dfacbasgrp  27376  lindsmm  27401  islinds3  27407  islindf4  27411  islnr3  27422  subrgacs  27611  sdrgacs  27612  isdomn3  27626  dvconstbi  27654  rfcnpre3  27807  rfcnpre4  27808  stoweidlem59  27911  3bior1fd  28177  3biant1d  28180  mpt2xopovel  28202  injresinj  28215  nbgrael  28275  nb3gra2nb  28291  nbcusgra  28298  trls  28335  istrl2  28337  0pth  28356  0spth  28357  wlkdvspthlem  28365  0crct  28371  0cycl  28372  sbc3org  28594  trsbc  28603  sbcssOLD  28605  bnj919  29113  bnj976  29125  bnj1542  29205  bnj150  29224  bnj151  29225  bnj607  29264  bnj852  29269  bnj873  29272  bnj938  29285  bnj1171  29346  bnj1388  29379  bnj1489  29402  equsalNEW7  29464  islshpat  29829  lcvbr2  29834  lcvbr3  29835  lshpsmreu  29921  isat3  30119  hlrelat5N  30212  islpln5  30346  cdlemblem  30604  paddvaln0N  30612  paddval0  30621  cdlemefrs29bpre1  31208  cdlemefrs29cpre1  31209  cdlemg27b  31507  cdlemg33c  31519  cdlemg33e  31521  diaglbN  31867  cdlemm10N  31930  dicopelval2  31993  dicelval2N  31994  dihopelvalcpre  32060  dihglbcpreN  32112  dih1dimatlem  32141  dihatexv  32150  dvh4dimlem  32255  mapdpglem3  32487  hdmap14lem13  32695  hdmapglem7a  32742
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 177
  Copyright terms: Public domain W3C validator