Theorem bitr2di 196

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

Hypotheses

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

Assertion

Ref	Expression
bitr2di	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem bitr2di

Step	Hyp	Ref	Expression
1		bitr2di.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr2di.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	bitrdi 195	. 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:  bitr4id  198  bibif  688  pm5.61  784  oranabs  805  pm5.7dc  944  nbbndc  1384  resopab2  4931  xpcom  5150  f1od2  6203  map1  6778  ac6sfi  6864  elznn0  9206  rexuz3  10932  xrmaxiflemcom  11190  metrest  13146  sincosq3sgn  13389  sincosq4sgn  13390