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  912  dn1dc  969  csbabg  3203  uniiunlem  3332  inimasn  5185  cnvpom  5310  fnresdisj  5473  f1oiso  6005  reldm  6393  mptelixpg  6982  1idprl  7921  1idpru  7922  nndiv  9298  fzn  10399  fz1sbc  10455  grpid  13797  znleval  14930  metrest  15500  loopclwwlkn1b  16543  clwwlknun  16565