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  899  dn1dc  955  csbabg  3110  uniiunlem  3236  inimasn  5028  cnvpom  5153  fnresdisj  5308  f1oiso  5805  reldm  6165  mptelixpg  6712  1idprl  7552  1idpru  7553  nndiv  8919  fzn  9998  fz1sbc  10052  grpid  12742  metrest  13300