Theorem syl5bbr 277

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

Hypotheses

Ref	Expression
syl5bbr.1	⊢ (𝜓 ↔ 𝜑)
syl5bbr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5bbr	⊢ (𝜒 → (𝜑 ↔ 𝜃))

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 216	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5bbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5bb 275	1 ⊢ (𝜒 → (𝜑 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3bitr3g  305  biass  377  19.16  2155  19.19  2159  sbbibOLD  2213  sbcom2  2408  sbcom2OLD  2409  sbal2  2494  sbal2OLD  2495  necon1bbid  3000  rspc2gv  3541  elabgt  3571  reuxfr4d  3648  sbceq1a  3688  sbcralt  3754  sbccsb2  4264  reuprg0  4506  disjxun  4921  dfres3  5693  xp11  5866  ressn  5968  fnssresb  6296  dmfco  6579  dffo4  6686  f1ompt  6692  funressn  6738  elunirnALT  6830  fliftf  6885  resoprab2  7081  elrnmpores  7098  ralrnmpo  7099  iunpw  7303  ordunisuc2  7369  tfis  7379  tfinds  7384  dfom2  7392  fun11iun  7452  opiota  7558  1stconst  7596  2ndconst  7597  fnsuppeq0  7654  iinon  7774  dfsmo2  7781  oeeui  8021  omabs  8066  brecop  8182  ixpsnf1o  8291  boxcutc  8294  ac6sfi  8549  wemapwe  8946  sdom2en01  9514  ac6num  9691  zorn2lem7  9714  ttukeylem6  9726  alephval2  9784  fpwwe2  9855  fpwwe  9858  nqereu  10141  suplem2pr  10265  map2psrpr  10322  supsrlem  10323  fimaxre3  11380  infm3  11393  crne0  11424  nn1suc  11454  xmulneg1  12471  supxrbnd1  12523  supxrbnd2  12524  iccneg  12667  wrdmap  13698  wrdind  13905  wrdindOLD  13906  rtrclreclem3  14270  cnpart  14450  sqrt00  14474  lo1resb  14772  o1resb  14774  absefib  15401  efieq1re  15402  sadadd2lem2  15649  saddisjlem  15663  prmind2  15875  isprm7  15898  mreacs  16777  issubc  16953  isfunc  16982  pospo  17431  mndind  17824  eqgval  18102  resscntz  18223  frgpuplem  18648  qusabl  18731  dmdprd  18860  dprdcntz2  18900  dprd2d2  18906  isnzr2  19747  mpfind  20019  gsummoncoe1  20165  pf1ind  20210  chrdvds  20367  chrcong  20368  znleval  20393  isphld  20490  smadiadetr  20978  mp2pm2mplem4  21111  isclo  21389  ist1-2  21649  isnrm2  21660  bwth  21712  nconnsubb  21725  subislly  21783  ptclsg  21917  qtopcld  22015  kqcldsat  22035  qustgplem  22422  tsmssubm  22444  ustuqtop  22548  utop2nei  22552  blval2  22865  caucfil  23579  ioorinv  23870  mbfss  23940  iblss2  24099  dvivthlem1  24298  lhop1  24304  deg1leb  24382  reeff1o  24728  sincosq3sgn  24779  sincosq4sgn  24780  dcubic  25115  efrlim  25239  fsumharmonic  25281  isppw  25383  issqf  25405  fsumdvdsmul  25464  ppiub  25472  lgsdinn0  25613  tglngne  26028  tgelrnln  26108  axlowdimlem14  26434  nbgrssovtx  26836  clwwlknclwwlkdif  27475  eupth2lem2  27739  fusgr2wsp2nb  27858  h2hlm  28526  isch2  28769  ch0pss  28993  nmcfnlbi  29600  jplem1  29816  hatomistici  29910  mdsymlem5  29955  cdjreui  29980  dfimafnf  30133  funcnvmpt  30164  fpwrelmap  30210  nn0min  30272  isarchi  30433  ordtconnlem1  30768  esumfsup  30930  esumpcvgval  30938  measvuni  31075  aean  31105  eulerpartlemgh  31238  ballotlemsima  31376  sgn3da  31402  bnj1468  31726  subfacp1lem2a  31972  subfacp1lem6  31977  eldm3  32457  onsuct0  33249  bj-restsn  33818  ptrest  34280  ptrecube  34281  poimirlem2  34283  poimirlem23  34304  sdclem2  34407  fdc  34410  fdc1  34411  istotbnd3  34439  sstotbnd  34443  prdstotbnd  34462  rrncmslem  34500  brinxprnres  34940  brcnvrabga  34993  alrmomodm  35007  br1cossxrnres  35081  lub0N  35718  glb0N  35722  cdlemefrs29bpre0  36925  dvhb1dimN  37515  dvhopellsm  37646  dibord  37688  dochnel2  37921  mapdvalc  38158  mapdval4N  38161  diophin  38710  diophun  38711  diophrex  38713  3rexfrabdioph  38735  6rexfrabdioph  38737  7rexfrabdioph  38738  zindbi  38884  rababg  39240  relexpnul  39331  clsk1independent  39704  scottabf  39896  hashnzfzclim  40014  fveqsb  40148  infxrbnd2  41012  cncfiooicclem1  41552  stoweidlem35  41697  tz6.12-afv  42724  ndmaovg  42735  tz6.12-afv2  42791  ich2exprop  42941  prprspr2  42988  line2x  44049  line2y  44050  itsclc0b  44067  aacllem  44209