Theorem syl6rbb 196

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

Hypotheses

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

Assertion

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

Proof of Theorem syl6rbb

Step	Hyp	Ref	Expression
1		syl6rbb.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6rbb.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	syl6bb 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  939  nbbndc  1373  resopab2  4874  xpcom  5093  f1od2  6140  map1  6714  ac6sfi  6800  elznn0  9093  rexuz3  10794  xrmaxiflemcom  11050  metrest  12714  sincosq3sgn  12957  sincosq4sgn  12958