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:  bitr3di  194  pm5.17dc  890  dn1dc  945  csbabg  3066  uniiunlem  3190  inimasn  4964  cnvpom  5089  fnresdisj  5241  f1oiso  5735  reldm  6092  mptelixpg  6636  1idprl  7422  1idpru  7423  nndiv  8785  fzn  9853  fz1sbc  9907  metrest  12714  bj-indeq  13298