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  1325  3biant1d  1328  clelab  2595  necon2abidOLD  2703  eueq3  3231  n0moeu  3748  sbcel12  3773  sbcel12gOLD  3774  sbceqg  3775  sbcne12  3777  sbcne12gOLD  3778  reldisj  3820  raldifeq  3866  r19.3rz  3869  r19.3rzv  3871  r19.9rzv  3872  eldifpr  3992  eldiftp  4017  reusv2lem5  4595  ordelpss  4845  rabxp  4973  elrng  5129  iss  5252  elimasni  5294  eliniseg  5296  xpcan  5372  xpcan2  5373  fcnvres  5686  dffv3  5785  funimass4  5841  fndmdif  5906  fneqeql  5910  funimass3  5918  elrnrexdmb  5947  dff4  5956  fconst4  6041  elunirn  6067  riota1  6170  riota2df  6172  f1ocnvfv3  6186  eqfnov  6296  elrnmpt2res  6304  caoftrn  6455  ordsucun  6536  dflim3  6558  dfom2  6578  peano5  6599  opiota  6733  suppssr  6820  mpt2xopovel  6837  brtpos  6854  rntpos  6858  ordgt0ge1  7037  ondif2  7042  oelim2  7134  omabs  7186  iiner  7272  erinxp  7274  qliftfun  7285  ordunifi  7663  elfi2  7765  elfiun  7781  fifo  7783  noinfep  7966  cantnfrescl  7985  cantnflem1  7998  cantnf  8002  cantnfOLD  8024  rankonidlem  8136  r1pwOLD  8154  pr2nelem  8272  cardalephex  8361  alephinit  8366  dfac5lem4  8397  cflim2  8533  cfsmolem  8540  compssiso  8644  fin1a2lem11  8680  itunisuc  8689  axdclem  8789  brdom6disj  8800  alephreg  8847  fpwwe2lem9  8906  pwfseqlem3  8928  pwfseqlem4  8930  indpi  9177  nqereu  9199  ordpinq  9213  ltanq  9241  ltmnq  9242  suplem2pr  9323  map2psrpr  9378  ssxr  9545  letri3  9561  leltne  9565  ltneg  9940  leneg  9943  suprnub  10394  negiso  10407  infmrgelb  10411  elnnnn0  10724  nn0sub  10731  zrevaddcl  10791  znnsub  10792  znn0sub  10793  prime  10823  eluz2  10968  indstr  11024  eluz2b1  11027  qrevaddcl  11076  rpneg  11121  xrleltne  11223  dfle2  11225  dflt2  11226  xrletri3  11230  supxrleub  11390  infmxrgelb  11398  ixxin  11418  iccid  11446  elicopnf  11486  iccsplit  11519  fzsplit2  11575  fzsn  11601  fzpr  11612  uzsplit  11631  injresinj  11740  om2uzf1oi  11877  lt2sqi  12055  le2sqi  12056  hashsdom  12246  hashf1lem1  12310  fz1isolem  12316  ccatlcan  12468  ccatrcan  12469  2swrd2eqwrdeq  12655  cnpart  12831  limsuplt  13059  rlimresb  13145  mertenslem2  13447  sadadd2lem2  13748  saddisjlem  13762  bitsuz  13772  gcddiv  13835  algcvgblem  13854  isprm2lem  13872  isprm3  13874  isprm5  13900  prmreclem5  14083  vdwapun  14137  vdwmc2  14142  ramcl  14192  pwsle  14532  ismre  14630  mreacs  14698  acsfn  14699  iscatd2  14721  cidpropd  14751  oppcsect2  14815  isfunc  14876  setcinv  15060  lubeldm  15253  lubval  15256  glbeldm  15266  glbval  15269  tosso  15308  ipodrsfi  15435  acsfiindd  15449  imasmnd2  15560  submacs  15595  imasgrp2  15772  issubg  15783  resgrpisgrp  15804  subgacs  15818  eqgval  15832  gaorber  15928  symgfix2  16023  psgnran  16123  isslw  16211  sylow2alem2  16221  sylow2a  16222  sylow3lem6  16235  efgcpbllemb  16356  prmcyg  16474  gsum2d2lem  16570  gsumcom2  16572  subgdmdprd  16636  dprd2d2  16648  pgpfac1lem2  16681  pgpfac1lem4  16684  imasrng  16817  drngmulne0  16960  lssle0  17137  lssacs  17154  lssats2  17187  lvecvsn0  17296  islpir  17437  isnzr2  17451  zndvds  18091  znleval  18096  znleval2  18097  lindsmm  18366  islinds3  18372  islindf4  18376  eltg2b  18680  discld  18809  opnssneib  18835  cldlp  18870  restbas  18878  leordtvallem1  18930  leordtvallem2  18931  ssidcn  18975  cnprest2  19010  lmss  19018  perfcls  19085  cmpfi  19127  1stccnp  19182  subislly  19201  hausmapdom  19220  iskgen3  19238  kgencn  19245  ptpjpre1  19260  xkoccn  19308  txrest  19320  txlm  19337  txkgen  19341  xkopt  19344  xkoinjcn  19376  imasnopn  19379  imasncld  19380  imasncls  19381  qtopcn  19403  kqfeq  19413  isr0  19426  fbfinnfr  19530  trfbas  19533  fbunfip  19558  ufileu  19608  cfinufil  19617  fmid  19649  txflf  19695  fclsrest  19713  alexsubALT  19739  tsmsresOLD  19833  tsmsres  19834  ucnima  19972  fmucndlem  19982  bldisj  20089  xmeter  20124  elbl4  20267  metuel2  20270  restmetu  20278  dscopn  20282  bl2ioo  20485  isphtpc  20682  tchcph  20868  lmmbr2  20886  lmmbrf  20889  iscau2  20904  iscauf  20907  caucfil  20910  metcld  20932  metcld2  20933  bcthlem1  20951  bcthlem4  20954  cldcss2  21045  ovolgelb  21079  ovoliunlem1  21101  ismbfcn  21225  mbfmax  21243  mbfimaopnlem  21249  i1faddlem  21287  i1fmullem  21288  i1fres  21299  i1fpos  21300  itg1climres  21308  xrge0f  21325  itgresr  21372  iblcnlem1  21381  limcun  21486  dvres  21502  mdegmullem  21665  ply1remlem  21750  plyremlem  21886  vieta1  21894  ulmcau  21976  sineq0  22099  coseq1  22100  ang180lem3  22323  cubic  22360  atandm  22387  atandm2  22388  atandm3  22389  rlimcnp  22475  rlimcnp2  22476  vmappw  22570  dchrelbas3  22693  dchrelbas4  22698  dchrsum2  22723  bposlem6  22744  dchrisumlem3  22856  pntleml  22976  lnrot2  23152  brbtwn2  23286  axsegconlem6  23303  axsegcon  23308  ax5seg  23319  axpasch  23322  axeuclid  23344  axcontlem4  23348  nbgrael  23472  nb3gra2nb  23498  nbcusgra  23506  trls  23570  istrl2  23572  is2wlk  23599  0pth  23604  0spth  23605  wlkdvspthlem  23641  0crct  23647  0cycl  23648  eupath2lem2  23734  elghom  23985  nmoolb  24306  nmlno0lem  24328  ubthlem1  24406  ocsh  24821  shle0  24980  eigrei  25373  adjeu  25428  nmoplb  25446  nmfnlb  25463  eleigvec2  25497  nmlnop0iALT  25534  cnlnadjlem5  25610  adjbdln  25622  jplem2  25808  cvbr2  25822  mdsl2bi  25862  chrelat3  25910  disjunsn  26070  ofpreima  26118  funcnvmpt  26121  funcnv5mpt  26122  dfcnv2  26128  gtiso  26130  fpwrelmap  26167  xrdifh  26204  fzsplit3  26212  toslublem  26262  tosglblem  26264  isarchi  26333  xrge0tsmsbi  26388  unitdivcld  26465  lmxrge0  26516  isrrext  26563  issibf  26853  eulerpartlemr  26891  eulerpartlemmf  26892  eulerpartlemn  26898  dstfrvunirn  26991  ballotlemfc0  27009  ballotlemfcc  27010  subfacp1lem3  27204  subfacp1lem5  27206  erdszelem9  27221  kur14  27238  iscvm  27282  dfpo2  27699  fundmpss  27711  opelco3  27723  dfon2  27739  elpredg  27773  preduz  27795  nofulllem1  27977  nofulllem2  27978  dfbigcup2  28064  sscoid  28078  funpartfv  28110  dfrdg4  28115  cgr3permute3  28212  segletr  28279  segleantisym  28280  seglelin  28281  cos2h  28561  tan2h  28562  mbfposadd  28577  cnambfre  28578  dvtanlem  28579  itg2addnclem  28581  itg2addnc  28584  iblabsnclem  28593  ftc1anclem1  28605  ftc1anclem5  28609  fneval  28697  locfindis  28715  neibastop3  28721  eltail  28733  filnetlem4  28740  caures  28794  heiborlem3  28850  heiborlem10  28857  divrngidl  28966  prtlem10  29148  prtlem16  29152  prtlem19  29161  prtex  29163  prter3  29165  isnacs2  29180  rabrenfdioph  29291  expdiophlem1  29508  pw2f1ocnv  29524  pwfi2f1o  29589  numinfctb  29597  dfacbasgrp  29602  islnr3  29609  subrgacs  29695  sdrgacs  29696  isdomn3  29710  dvconstbi  29746  rfcnpre3  29893  rfcnpre4  29894  stoweidlem59  29992  otthg  30268  f12dfv  30284  wlkcomp  30424  el2wlkonotot0  30529  2wot2wont  30543  usg2spthonot1  30547  2spot2iun2spont  30548  clwlkcomp  30564  clwlkisclwwlklem0  30588  clwlkisclwwlk  30589  isrusgra  30682  rusgranumwlks  30712  vdn1frgrav2  30756  vdgn1frgrav2  30757  usgreg2spot  30798  numclwwlkovgel  30819  scmatscmids  31014  sbc3orgOLD  31538  sbcssOLD  31549  bnj919  32060  bnj976  32071  bnj1542  32150  bnj150  32169  bnj151  32170  bnj607  32209  bnj852  32214  bnj873  32217  bnj938  32230  bnj1171  32291  bnj1388  32324  bnj1489  32347  bj-hbntbi  32494  bj-sbceqgALT  32704  islshpat  32968  lcvbr2  32973  lcvbr3  32974  lshpsmreu  33060  isat3  33258  hlrelat5N  33351  islpln5  33485  cdlemblem  33743  paddvaln0N  33751  paddval0  33760  cdlemefrs29bpre1  34347  cdlemefrs29cpre1  34348  cdlemg27b  34646  cdlemg33c  34658  cdlemg33e  34660  diaglbN  35006  cdlemm10N  35069  dicopelval2  35132  dicelval2N  35133  dihopelvalcpre  35199  dihglbcpreN  35251  dih1dimatlem  35280  dihatexv  35289  dvh4dimlem  35394  mapdpglem3  35626  hdmap14lem13  35834  hdmapglem7a  35881