Theorem bitr2id 193

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	bitrid 192	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜃))
4	3	bicomd 141	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr3di  195  pm5.17dc  911  dn1dc  968  csbabg  3188  uniiunlem  3315  inimasn  5156  cnvpom  5281  fnresdisj  5444  f1oiso  5972  reldm  6354  mptelixpg  6908  1idprl  7815  1idpru  7816  nndiv  9189  fzn  10282  fz1sbc  10336  grpid  13645  znleval  14691  metrest  15259  loopclwwlkn1b  16299  clwwlknun  16321