Theorem syl6rbb 291

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr4id  293  bibif  375  oranabs  997  necon4bid  3032  2reu4lem  4423  resopab2  5871  xpco  6108  funconstss  6803  xpopth  7712  snmapen  8573  ac6sfi  8746  supgtoreq  8918  rankr1bg  9216  alephsdom  9497  brdom7disj  9942  fpwwe2lem13  10053  nn0sub  11935  elznn0  11984  nn01to3  12329  supxrbnd1  12702  supxrbnd2  12703  rexuz3  14700  smueqlem  15829  qnumdenbi  16074  dfiso3  17035  lssne0  19715  pjfval2  20398  0top  21588  1stccn  22068  dscopn  23180  bcthlem1  23928  ovolgelb  24084  iblpos  24396  itgposval  24399  itgsubstlem  24651  sincosq3sgn  25093  sincosq4sgn  25094  lgsquadlem3  25966  colinearalg  26704  elntg2  26779  wlklnwwlkln2lem  27668  2pthdlem1  27716  wwlks2onsym  27744  rusgrnumwwlkb0  27757  numclwwlk2lem1  28161  nmoo0  28574  leop3  29908  leoptri  29919  f1od2  30483  tltnle  30675  fedgmullem2  31114  dfrdg4  33525  curf  35035  poimirlem28  35085  itgaddnclem2  35116  lfl1dim  36417  glbconxN  36674  2dim  36766  elpadd0  37105  dalawlem13  37179  diclspsn  38490  dihglb2  38638  dochsordN  38670  lzunuz  39709  uneqsn  40726  ntrclskb  40772  ntrneiel2  40789  infxrbnd2  42001  funressnfv  43635  funressndmafv2rn  43779  iccpartiltu  43939