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  1329  3biant1d  1332  clelab  2604  necon2abidOLD  2715  eueq3  3271  n0moeu  3791  sbcel12  3816  sbcel12gOLD  3817  sbceqg  3818  sbcne12  3820  sbcne12gOLD  3821  reldisj  3863  raldifeq  3909  r19.3rz  3912  r19.3rzv  3914  r19.9rzv  3915  eldifpr  4037  eldiftp  4063  reusv2lem5  4645  otthg  4723  ordelpss  4899  rabxp  5028  elrng  5185  iss  5312  elimasni  5355  eliniseg  5357  xpcan  5434  xpcan2  5435  fcnvres  5753  dffv3  5853  funimass4  5909  fndmdif  5976  fneqeql  5980  funimass3  5988  elrnrexdmb  6017  dff4  6026  fconst4  6116  elunirn  6142  f12dfv  6158  riota1  6255  riota2df  6257  f1ocnvfv3  6271  eqfnov  6383  elrnmpt2res  6391  caoftrn  6550  ordsucun  6631  dflim3  6653  dfom2  6673  peano5  6694  opiota  6833  suppssr  6921  mpt2xopovel  6938  brtpos  6954  rntpos  6958  ordgt0ge1  7137  ondif2  7142  oelim2  7234  omabs  7286  iiner  7373  erinxp  7375  qliftfun  7386  ordunifi  7759  elfi2  7863  elfiun  7879  fifo  7881  noinfep  8065  cantnfrescl  8084  cantnflem1  8097  cantnf  8101  cantnfOLD  8123  rankonidlem  8235  r1pwOLD  8253  pr2nelem  8371  cardalephex  8460  alephinit  8465  dfac5lem4  8496  cflim2  8632  cfsmolem  8639  compssiso  8743  fin1a2lem11  8779  itunisuc  8788  axdclem  8888  brdom6disj  8899  alephreg  8946  fpwwe2lem9  9005  pwfseqlem3  9027  pwfseqlem4  9029  indpi  9274  nqereu  9296  ordpinq  9310  ltanq  9338  ltmnq  9339  suplem2pr  9420  map2psrpr  9476  ssxr  9643  letri3  9659  leltne  9663  ltneg  10041  leneg  10044  suprnub  10495  negiso  10508  infmrgelb  10512  elnnnn0  10828  nn0sub  10835  zrevaddcl  10897  znnsub  10898  znn0sub  10899  prime  10930  eluz2  11077  indstr  11139  eluz2b1  11142  qrevaddcl  11193  rpneg  11238  xrleltne  11340  dfle2  11342  dflt2  11343  xrletri3  11347  supxrleub  11507  infmxrgelb  11515  ixxin  11535  iccid  11563  elicopnf  11609  iccsplit  11642  fzsplit2  11699  fzsn  11714  fzpr  11724  uzsplit  11739  injresinj  11883  om2uzf1oi  12020  lt2sqi  12211  le2sqi  12212  hashsdom  12404  hashf1lem1  12457  fz1isolem  12463  ccatlcan  12647  ccatrcan  12648  2swrd2eqwrdeq  12841  cnpart  13023  limsuplt  13251  rlimresb  13337  mertenslem2  13646  sadadd2lem2  13948  saddisjlem  13962  bitsuz  13972  gcddiv  14035  algcvgblem  14054  isprm2lem  14072  isprm3  14074  isprm5  14101  prmreclem5  14286  vdwapun  14340  vdwmc2  14345  ramcl  14395  pwsle  14736  ismre  14834  mreacs  14902  acsfn  14903  iscatd2  14925  cidpropd  14955  oppcsect2  15019  isfunc  15080  setcinv  15264  lubeldm  15457  lubval  15460  glbeldm  15470  glbval  15473  tosso  15512  ipodrsfi  15639  acsfiindd  15653  imasmnd2  15764  submacs  15799  imasgrp2  15978  issubg  15989  resgrpisgrp  16010  subgacs  16024  eqgval  16038  gaorber  16134  symgfix2  16229  psgnran  16329  isslw  16417  sylow2alem2  16427  sylow2a  16428  sylow3lem6  16441  efgcpbllemb  16562  prmcyg  16680  gsum2d2lem  16785  gsumcom2  16787  subgdmdprd  16864  dprd2d2  16876  pgpfac1lem2  16909  pgpfac1lem4  16912  imasrng  17045  drngmulne0  17194  lssle0  17372  lssacs  17389  lssats2  17422  lvecvsn0  17531  islpir  17672  isnzr2  17686  zndvds  18348  znleval  18353  znleval2  18354  lindsmm  18623  islinds3  18629  islindf4  18633  eltg2b  19220  discld  19349  opnssneib  19375  cldlp  19410  restbas  19418  leordtvallem1  19470  leordtvallem2  19471  ssidcn  19515  cnprest2  19550  lmss  19558  perfcls  19625  cmpfi  19667  1stccnp  19722  subislly  19741  hausmapdom  19760  iskgen3  19778  kgencn  19785  ptpjpre1  19800  xkoccn  19848  txrest  19860  txlm  19877  txkgen  19881  xkopt  19884  xkoinjcn  19916  imasnopn  19919  imasncld  19920  imasncls  19921  qtopcn  19943  kqfeq  19953  isr0  19966  fbfinnfr  20070  trfbas  20073  fbunfip  20098  ufileu  20148  cfinufil  20157  fmid  20189  txflf  20235  fclsrest  20253  alexsubALT  20279  tsmsresOLD  20373  tsmsres  20374  ucnima  20512  fmucndlem  20522  bldisj  20629  xmeter  20664  elbl4  20807  metuel2  20810  restmetu  20818  dscopn  20822  bl2ioo  21025  isphtpc  21222  tchcph  21408  lmmbr2  21426  lmmbrf  21429  iscau2  21444  iscauf  21447  caucfil  21450  metcld  21472  metcld2  21473  bcthlem1  21491  bcthlem4  21494  cldcss2  21585  ovolgelb  21619  ovoliunlem1  21641  ismbfcn  21766  mbfmax  21784  mbfimaopnlem  21790  i1faddlem  21828  i1fmullem  21829  i1fres  21840  i1fpos  21841  itg1climres  21849  xrge0f  21866  itgresr  21913  iblcnlem1  21922  limcun  22027  dvres  22043  mdegmullem  22206  ply1remlem  22291  plyremlem  22427  vieta1  22435  ulmcau  22517  sineq0  22640  coseq1  22641  ang180lem3  22864  cubic  22901  atandm  22928  atandm2  22929  atandm3  22930  rlimcnp  23016  rlimcnp2  23017  vmappw  23111  dchrelbas3  23234  dchrelbas4  23239  dchrsum2  23264  bposlem6  23285  dchrisumlem3  23397  pntleml  23517  lnrot2  23711  islmib  23823  brbtwn2  23877  axsegconlem6  23894  axsegcon  23899  ax5seg  23910  axpasch  23913  axeuclid  23935  axcontlem4  23939  usgracl  24014  elusuhgra  24030  nbgrael  24088  nb3gra2nb  24117  nbcusgra  24125  wlkcomp  24187  trls  24200  istrl2  24202  is2wlk  24229  0pth  24234  0spth  24235  wlkdvspthlem  24271  0crct  24288  0cycl  24289  clwlkcomp  24425  clwlkisclwwlklem0  24450  clwlkisclwwlk  24451  el2wlkonotot0  24534  2wot2wont  24548  usg2spthonot1  24552  2spot2iun2spont  24553  isrusgra  24589  isrusgusrgcl  24595  isrusgracl  24597  0eusgraiff0rgracl  24603  rusgranumwlks  24618  eupath2lem2  24640  elghom  24891  nmoolb  25212  nmlno0lem  25234  ubthlem1  25312  ocsh  25727  shle0  25886  eigrei  26279  adjeu  26334  nmoplb  26352  nmfnlb  26369  eleigvec2  26403  nmlnop0iALT  26440  cnlnadjlem5  26516  adjbdln  26528  jplem2  26714  cvbr2  26728  mdsl2bi  26768  chrelat3  26816  disjunsn  26976  opeldifid  26979  ofpreima  27029  funcnvmpt  27032  funcnv5mpt  27033  dfcnv2  27039  gtiso  27041  fpwrelmap  27078  xrdifh  27109  fzsplit3  27117  toslublem  27167  tosglblem  27169  isarchi  27238  xrge0tsmsbi  27289  unitdivcld  27369  lmxrge0  27420  isrrext  27467  issibf  27765  eulerpartlemr  27803  eulerpartlemmf  27804  eulerpartlemn  27810  dstfrvunirn  27903  ballotlemfc0  27921  ballotlemfcc  27922  subfacp1lem3  28116  subfacp1lem5  28118  erdszelem9  28133  kur14  28150  iscvm  28194  dfpo2  28611  fundmpss  28623  opelco3  28635  dfon2  28651  elpredg  28685  preduz  28707  nofulllem1  28889  nofulllem2  28890  dfbigcup2  28976  sscoid  28990  funpartfv  29022  dfrdg4  29027  cgr3permute3  29124  segletr  29191  segleantisym  29192  seglelin  29193  cos2h  29474  tan2h  29475  mbfposadd  29490  cnambfre  29491  dvtanlem  29492  itg2addnclem  29494  itg2addnc  29497  iblabsnclem  29506  ftc1anclem1  29518  ftc1anclem5  29522  fneval  29610  locfindis  29628  neibastop3  29634  eltail  29646  filnetlem4  29653  caures  29707  heiborlem3  29763  heiborlem10  29770  divrngidl  29879  prtlem10  30061  prtlem16  30065  prtlem19  30074  prtex  30076  prter3  30078  isnacs2  30093  rabrenfdioph  30203  expdiophlem1  30420  pw2f1ocnv  30436  pwfi2f1o  30501  numinfctb  30509  dfacbasgrp  30514  islnr3  30521  subrgacs  30607  sdrgacs  30608  isdomn3  30622  dvconstbi  30658  rfcnpre3  30805  rfcnpre4  30806  unima  30838  cncfshift  31031  stoweidlem59  31178  prelpw  31585  uhgrasiz  31661  isfusgracl  31692  fusgraimpclALT  31694  usgfis  31704  vdn1frgrav2  31744  vdgn1frgrav2  31745  usgreg2spot  31786  numclwwlkovgel  31807  sbc3orgOLD  32257  sbcssOLD  32268  bnj919  32779  bnj976  32790  bnj1542  32869  bnj150  32888  bnj151  32889  bnj607  32928  bnj852  32933  bnj873  32936  bnj938  32949  bnj1171  33010  bnj1388  33043  bnj1489  33066  bj-hbntbi  33215  bj-sbceqgALT  33425  islshpat  33689  lcvbr2  33694  lcvbr3  33695  lshpsmreu  33781  isat3  33979  hlrelat5N  34072  islpln5  34206  cdlemblem  34464  paddvaln0N  34472  paddval0  34481  cdlemefrs29bpre1  35068  cdlemefrs29cpre1  35069  cdlemg27b  35367  cdlemg33c  35379  cdlemg33e  35381  diaglbN  35727  cdlemm10N  35790  dicopelval2  35853  dicelval2N  35854  dihopelvalcpre  35920  dihglbcpreN  35972  dih1dimatlem  36001  dihatexv  36010  dvh4dimlem  36115  mapdpglem3  36347  hdmap14lem13  36555  hdmapglem7a  36602