Theorem syl6rbb 290

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

Hypotheses

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

Assertion

Ref	Expression
syl6rbb	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem syl6rbb

Step	Hyp	Ref	Expression
1		syl6rbb.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6rbb.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	syl6bb 289	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 225	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl6rbbr  292  bibif  374  oranabs  996  necon4bid  3061  2reu4lem  4465  resopab2  5904  xpco  6140  funconstss  6826  xpopth  7730  snmapen  8590  ac6sfi  8762  supgtoreq  8934  rankr1bg  9232  alephsdom  9512  brdom7disj  9953  fpwwe2lem13  10064  nn0sub  11948  elznn0  11997  nn01to3  12342  supxrbnd1  12715  supxrbnd2  12716  rexuz3  14708  smueqlem  15839  qnumdenbi  16084  dfiso3  17043  lssne0  19722  pjfval2  20853  0top  21591  1stccn  22071  dscopn  23183  bcthlem1  23927  ovolgelb  24081  iblpos  24393  itgposval  24396  itgsubstlem  24645  sincosq3sgn  25086  sincosq4sgn  25087  lgsquadlem3  25958  colinearalg  26696  elntg2  26771  wlklnwwlkln2lem  27660  2pthdlem1  27709  wwlks2onsym  27737  rusgrnumwwlkb0  27750  numclwwlk2lem1  28155  nmoo0  28568  leop3  29902  leoptri  29913  f1od2  30457  tltnle  30649  fedgmullem2  31026  dfrdg4  33412  curf  34885  poimirlem28  34935  itgaddnclem2  34966  lfl1dim  36272  glbconxN  36529  2dim  36621  elpadd0  36960  dalawlem13  37034  diclspsn  38345  dihglb2  38493  dochsordN  38525  lzunuz  39385  uneqsn  40393  ntrclskb  40439  ntrneiel2  40456  infxrbnd2  41657  funressnfv  43298  funressndmafv2rn  43442  iccpartiltu  43602