Theorem syl5rbbr 193

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
syl5rbbr	⊢ (𝜒 → (𝜃 ↔ 𝜑))

Proof of Theorem syl5rbbr

Step	Hyp	Ref	Expression
1		syl5rbbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 130	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5rbbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5rbb 191	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  xordc  1323  sbal2  1939  eqsnm  3547  fnressn  5370  fressnfv  5371  eluniimadm  5425  genpassl  6714  genpassu  6715  1idprl  6780  1idpru  6781  axcaucvglemres  7065  negeq0  7362  muleqadd  7758  crap0  8035  addltmul  8267  fzrev  9101  modq0  9331  cjap0  9794  cjne0  9795  caucvgrelemrec  9865  lenegsq  9981  dvdsabseq  10247  elabgf0  10587