Theorem syl5rbbr 194

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 131	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5rbbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5rbb 192	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:  xordc  1370  sbal2  1997  eqsnm  3682  fnressn  5606  fressnfv  5607  eluniimadm  5666  genpassl  7332  genpassu  7333  1idprl  7398  1idpru  7399  axcaucvglemres  7707  negeq0  8016  muleqadd  8429  crap0  8716  addltmul  8956  fzrev  9864  modq0  10102  cjap0  10679  cjne0  10680  caucvgrelemrec  10751  lenegsq  10867  isumss  11160  fsumsplit  11176  sumsplitdc  11201  dvdsabseq  11545  oddennn  11905  metrest  12675  elabgf0  12984