Theorem syl5rbb 192

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-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 191	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 140	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5rbbr  194  pm5.17dc  889  dn1dc  944  csbabg  3061  uniiunlem  3185  inimasn  4956  cnvpom  5081  fnresdisj  5233  f1oiso  5727  reldm  6084  mptelixpg  6628  1idprl  7398  1idpru  7399  nndiv  8761  fzn  9822  fz1sbc  9876  metrest  12675  bj-indeq  13127