Theorem bitr2id 192

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr2id

Step	Hyp	Ref	Expression
1		bitr2id.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2id.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  894  dn1dc  950  csbabg  3106  uniiunlem  3231  inimasn  5021  cnvpom  5146  fnresdisj  5298  f1oiso  5794  reldm  6154  mptelixpg  6700  1idprl  7531  1idpru  7532  nndiv  8898  fzn  9977  fz1sbc  10031  metrest  13156