Theorem syl5rbb 286

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		syl5rbb.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5bb 285	. 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:  syl5rbbr  288  necon1abid  3057  necon4abid  3059  uniiunlem  4064  r19.9rzv  4448  2reu4lem  4468  inimasn  6016  fnresdisj  6470  f1oiso  7107  reldm  7746  rdglim2  8071  mptelixpg  8502  1idpr  10454  nndiv  11686  fz1sbc  12986  grpid  18142  znleval  20704  fbunfip  22480  lmflf  22616  metcld2  23913  lgsne0  25914  isuvtx  27180  loopclwwlkn1b  27823  clwwlknun  27894  frgrncvvdeqlem2  28082  isph  28602  ofpreima  30413  eulerpartlemd  31628  bnj168  32004  opelco3  33022  wl-2sb6d  34798  poimirlem26  34922  cnambfre  34944  heibor1  35092  opltn0  36330  cvrnbtwn2  36415  cvrnbtwn4  36419  atlltn0  36446  pmapjat1  36993  dih1dimatlem  38469  2rexfrabdioph  39399  dnwech  39654  rfovcnvf1od  40356  uneqsn  40379  lighneallem2  43778  isrnghm  44170  rnghmval2  44173