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:  syl6rbbr  198  bibif  687  pm5.61  783  oranabs  804  pm5.7dc  938  nbbndc  1372  resopab2  4861  xpcom  5080  f1od2  6125  map1  6699  ac6sfi  6785  elznn0  9062  rexuz3  10755  xrmaxiflemcom  11011  metrest  12664  sincosq3sgn  12898  sincosq4sgn  12899