Theorem syl6bbr 263

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
syl6bbr.1	|- ( ph -> ( ps <-> ch ) )
syl6bbr.2	|- ( th <-> ch )

Assertion

Ref	Expression
syl6bbr	|- ( ph -> ( ps <-> th ) )

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		syl6bbr.2	. . 3 |- ( th <-> ch )
3	2	bicomi 202	. 2 |- ( ch <-> th )
4	1, 3	syl6bb 261	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 184

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

This theorem is referenced by:  3bitr4g  288  bibi2i  313  mtt  339  nbn2  345  3bior1fd  1324  3biant1d  1327  necon2abid  2663  eueq3  3129  n0moeu  3645  sbcel12  3670  sbcel12gOLD  3671  sbceqg  3672  sbcne12  3674  sbcne12gOLD  3675  reldisj  3717  raldifeq  3763  r19.3rz  3766  r19.3rzv  3768  r19.9rzv  3769  eldifpr  3889  eldiftp  3914  reusv2lem5  4492  ordelpss  4742  rabxp  4870  elrng  5026  iss  5149  elimasni  5191  eliniseg  5193  xpcan  5269  xpcan2  5270  fcnvres  5583  dffv3  5682  funimass4  5737  fndmdif  5802  fneqeql  5806  funimass3  5814  elrnrexdmb  5843  dff4  5852  fconst4  5937  elunirn  5963  riota1  6066  riota2df  6068  f1ocnvfv3  6082  eqfnov  6191  elrnmpt2res  6199  caoftrn  6350  ordsucun  6431  dflim3  6453  dfom2  6473  peano5  6494  opiota  6628  suppssr  6715  mpt2xopovel  6732  brtpos  6749  rntpos  6753  ordgt0ge1  6929  ondif2  6934  oelim2  7026  omabs  7078  iiner  7164  erinxp  7166  qliftfun  7177  ordunifi  7554  elfi2  7656  elfiun  7672  fifo  7674  noinfep  7857  cantnfrescl  7876  cantnflem1  7889  cantnf  7893  cantnfOLD  7915  rankonidlem  8027  r1pwOLD  8045  pr2nelem  8163  cardalephex  8252  alephinit  8257  dfac5lem4  8288  cflim2  8424  cfsmolem  8431  compssiso  8535  fin1a2lem11  8571  itunisuc  8580  axdclem  8680  brdom6disj  8691  alephreg  8738  fpwwe2lem9  8797  pwfseqlem3  8819  pwfseqlem4  8821  indpi  9068  nqereu  9090  ordpinq  9104  ltanq  9132  ltmnq  9133  suplem2pr  9214  map2psrpr  9269  ssxr  9436  letri3  9452  leltne  9456  ltneg  9831  leneg  9834  suprnub  10285  negiso  10298  infmrgelb  10302  elnnnn0  10615  nn0sub  10622  zrevaddcl  10682  znnsub  10683  znn0sub  10684  prime  10714  eluz2  10859  indstr  10915  eluz2b1  10918  qrevaddcl  10967  rpneg  11012  xrleltne  11114  dfle2  11116  dflt2  11117  xrletri3  11121  supxrleub  11281  infmxrgelb  11289  ixxin  11309  iccid  11337  elicopnf  11377  iccsplit  11410  fzsplit2  11466  fzsn  11492  fzpr  11503  uzsplit  11522  injresinj  11631  om2uzf1oi  11768  lt2sqi  11946  le2sqi  11947  hashsdom  12136  hashf1lem1  12200  fz1isolem  12206  ccatlcan  12358  ccatrcan  12359  2swrd2eqwrdeq  12545  cnpart  12721  limsuplt  12949  rlimresb  13035  mertenslem2  13337  sadadd2lem2  13638  saddisjlem  13652  bitsuz  13662  gcddiv  13725  algcvgblem  13744  isprm2lem  13762  isprm3  13764  isprm5  13790  prmreclem5  13973  vdwapun  14027  vdwmc2  14032  ramcl  14082  pwsle  14422  ismre  14520  mreacs  14588  acsfn  14589  iscatd2  14611  cidpropd  14641  oppcsect2  14705  isfunc  14766  setcinv  14950  lubeldm  15143  lubval  15146  glbeldm  15156  glbval  15159  tosso  15198  ipodrsfi  15325  acsfiindd  15339  imasmnd2  15450  submacs  15484  imasgrp2  15661  issubg  15672  resgrpisgrp  15693  subgacs  15707  eqgval  15721  gaorber  15817  symgfix2  15912  psgnran  16012  isslw  16098  sylow2alem2  16108  sylow2a  16109  sylow3lem6  16122  efgcpbllemb  16243  prmcyg  16361  gsum2d2lem  16455  gsumcom2  16457  subgdmdprd  16521  dprd2d2  16533  pgpfac1lem2  16566  pgpfac1lem4  16569  imasrng  16701  drngmulne0  16834  lssle0  17011  lssacs  17028  lssats2  17061  lvecvsn0  17170  islpir  17311  isnzr2  17325  zndvds  17962  znleval  17967  znleval2  17968  lindsmm  18237  islinds3  18243  islindf4  18247  eltg2b  18544  discld  18673  opnssneib  18699  cldlp  18734  restbas  18742  leordtvallem1  18794  leordtvallem2  18795  ssidcn  18839  cnprest2  18874  lmss  18882  perfcls  18949  cmpfi  18991  1stccnp  19046  subislly  19065  hausmapdom  19084  iskgen3  19102  kgencn  19109  ptpjpre1  19124  xkoccn  19172  txrest  19184  txlm  19201  txkgen  19205  xkopt  19208  xkoinjcn  19240  imasnopn  19243  imasncld  19244  imasncls  19245  qtopcn  19267  kqfeq  19277  isr0  19290  fbfinnfr  19394  trfbas  19397  fbunfip  19422  ufileu  19472  cfinufil  19481  fmid  19513  txflf  19559  fclsrest  19577  alexsubALT  19603  tsmsresOLD  19697  tsmsres  19698  ucnima  19836  fmucndlem  19846  bldisj  19953  xmeter  19988  elbl4  20131  metuel2  20134  restmetu  20142  dscopn  20146  bl2ioo  20349  isphtpc  20546  tchcph  20732  lmmbr2  20750  lmmbrf  20753  iscau2  20768  iscauf  20771  caucfil  20774  metcld  20796  metcld2  20797  bcthlem1  20815  bcthlem4  20818  cldcss2  20909  ovolgelb  20943  ovoliunlem1  20965  ismbfcn  21089  mbfmax  21107  mbfimaopnlem  21113  i1faddlem  21151  i1fmullem  21152  i1fres  21163  i1fpos  21164  itg1climres  21172  xrge0f  21189  itgresr  21236  iblcnlem1  21245  limcun  21350  dvres  21366  mdegmullem  21529  ply1remlem  21614  plyremlem  21750  vieta1  21758  ulmcau  21840  sineq0  21963  coseq1  21964  ang180lem3  22187  cubic  22224  atandm  22251  atandm2  22252  atandm3  22253  rlimcnp  22339  rlimcnp2  22340  vmappw  22434  dchrelbas3  22557  dchrelbas4  22562  dchrsum2  22587  bposlem6  22608  dchrisumlem3  22720  pntleml  22840  lnrot2  23011  brbtwn2  23119  axsegconlem6  23136  axsegcon  23141  ax5seg  23152  axpasch  23155  axeuclid  23177  axcontlem4  23181  nbgrael  23305  nb3gra2nb  23331  nbcusgra  23339  trls  23403  istrl2  23405  is2wlk  23432  0pth  23437  0spth  23438  wlkdvspthlem  23474  0crct  23480  0cycl  23481  eupath2lem2  23567  elghom  23818  nmoolb  24139  nmlno0lem  24161  ubthlem1  24239  ocsh  24654  shle0  24813  eigrei  25206  adjeu  25261  nmoplb  25279  nmfnlb  25296  eleigvec2  25330  nmlnop0iALT  25367  cnlnadjlem5  25443  adjbdln  25455  jplem2  25641  cvbr2  25655  mdsl2bi  25695  chrelat3  25743  disjunsn  25904  ofpreima  25952  funcnvmpt  25955  funcnv5mpt  25956  dfcnv2  25962  gtiso  25964  fpwrelmap  26001  xrdifh  26038  fzsplit3  26046  toslublem  26096  tosglblem  26098  isarchi  26167  xrge0tsmsbi  26222  unitdivcld  26300  lmxrge0  26351  isrrext  26398  issibf  26688  eulerpartlemr  26726  eulerpartlemmf  26727  eulerpartlemn  26733  dstfrvunirn  26826  ballotlemfc0  26844  ballotlemfcc  26845  subfacp1lem3  27039  subfacp1lem5  27041  erdszelem9  27056  kur14  27073  iscvm  27117  dfpo2  27534  fundmpss  27546  opelco3  27558  dfon2  27574  elpredg  27608  preduz  27630  nofulllem1  27812  nofulllem2  27813  dfbigcup2  27899  sscoid  27913  funpartfv  27945  dfrdg4  27950  cgr3permute3  28047  segletr  28114  segleantisym  28115  seglelin  28116  cos2h  28394  tan2h  28395  mbfposadd  28410  cnambfre  28411  dvtanlem  28412  itg2addnclem  28414  itg2addnc  28417  iblabsnclem  28426  ftc1anclem1  28438  ftc1anclem5  28442  fneval  28530  locfindis  28548  neibastop3  28554  eltail  28566  filnetlem4  28573  caures  28627  heiborlem3  28683  heiborlem10  28690  divrngidl  28799  prtlem10  28981  prtlem16  28985  prtlem19  28994  prtex  28996  prter3  28998  isnacs2  29013  rabrenfdioph  29124  expdiophlem1  29341  pw2f1ocnv  29357  pwfi2f1o  29422  numinfctb  29430  dfacbasgrp  29435  islnr3  29442  subrgacs  29528  sdrgacs  29529  isdomn3  29543  dvconstbi  29579  rfcnpre3  29726  rfcnpre4  29727  stoweidlem59  29825  otthg  30101  f12dfv  30117  wlkcomp  30257  el2wlkonotot0  30362  2wot2wont  30376  usg2spthonot1  30380  2spot2iun2spont  30381  clwlkcomp  30397  clwlkisclwwlklem0  30421  clwlkisclwwlk  30422  isrusgra  30515  rusgranumwlks  30545  vdn1frgrav2  30589  vdgn1frgrav2  30590  usgreg2spot  30631  numclwwlkovgel  30652  sbc3orgOLD  31167  sbcssOLD  31178  bnj919  31689  bnj976  31700  bnj1542  31779  bnj150  31798  bnj151  31799  bnj607  31838  bnj852  31843  bnj873  31846  bnj938  31859  bnj1171  31920  bnj1388  31953  bnj1489  31976  bj-sbceqgALT  32304  islshpat  32555  lcvbr2  32560  lcvbr3  32561  lshpsmreu  32647  isat3  32845  hlrelat5N  32938  islpln5  33072  cdlemblem  33330  paddvaln0N  33338  paddval0  33347  cdlemefrs29bpre1  33934  cdlemefrs29cpre1  33935  cdlemg27b  34233  cdlemg33c  34245  cdlemg33e  34247  diaglbN  34593  cdlemm10N  34656  dicopelval2  34719  dicelval2N  34720  dihopelvalcpre  34786  dihglbcpreN  34838  dih1dimatlem  34867  dihatexv  34876  dvh4dimlem  34981  mapdpglem3  35213  hdmap14lem13  35421  hdmapglem7a  35468