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 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr3di  195  pm5.17dc  916  dn1dc  973  csbabg  3209  uniiunlem  3338  inimasn  5208  cnvpom  5333  fnresdisj  5496  f1oiso  6035  reldm  6424  mptelixpg  7021  1idprl  7964  1idpru  7965  nndiv  9355  fzn  10464  fz1sbc  10521  grpid  13904  znleval  15098  metrest  15744  loopclwwlkn1b  16877  clwwlknun  16899