Theorem syl6rbb 276

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 275	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 212	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  syl6rbbr  278  bibif  360  pm5.61  745  oranabs  897  necon4bid  2827  resopab2  5368  xpco  5592  funconstss  6243  xpopth  7098  map1  7921  ac6sfi  8089  supgtoreq  8259  rankr1bg  8549  alephsdom  8792  brdom7disj  9234  fpwwe2lem13  9343  nn0sub  11220  elznn0  11269  nn01to3  11657  supxrbnd1  12023  supxrbnd2  12024  rexuz3  13936  smueqlem  15050  qnumdenbi  15290  dfiso3  16256  lssne0  18772  pjfval2  19872  0top  20598  1stccn  21076  dscopn  22188  bcthlem1  22929  ovolgelb  23055  iblpos  23365  itgposval  23368  itgsubstlem  23615  sincosq3sgn  24056  sincosq4sgn  24057  lgsquadlem3  24907  colinearalg  25590  wlklniswwlkn2  26228  rusgranumwlkb0  26480  usgreg2spot  26594  extwwlkfab  26617  numclwwlk2lem1  26629  nmoo0  27030  leop3  28368  leoptri  28379  f1od2  28887  tltnle  28993  nofulllem5  31105  dfrdg4  31228  curf  32557  poimirlem28  32607  itgaddnclem2  32639  lfl1dim  33426  glbconxN  33682  2dim  33774  elpadd0  34113  dalawlem13  34187  diclspsn  35501  dihglb2  35649  dochsordN  35681  lzunuz  36349  uneqsn  37341  ntrclskb  37387  ntrneiel2  37404  infxrbnd2  38526  2reu4a  39838  funressnfv  39857  iccpartiltu  39960  1wlklnwwlkln2lem  41079  2pthdlem1  41137  rusgrnumwwlkb0  41174  fusgreg2wsp  41500  av-numclwwlk2lem1  41532