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  1995  eqsnm  3677  fnressn  5599  fressnfv  5600  eluniimadm  5659  genpassl  7325  genpassu  7326  1idprl  7391  1idpru  7392  axcaucvglemres  7700  negeq0  8009  muleqadd  8422  crap0  8709  addltmul  8949  fzrev  9857  modq0  10095  cjap0  10672  cjne0  10673  caucvgrelemrec  10744  lenegsq  10860  isumss  11153  fsumsplit  11169  sumsplitdc  11194  dvdsabseq  11534  oddennn  11894  metrest  12664  elabgf0  12973