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  1328  sbal2  1946  eqsnm  3599  fnressn  5483  fressnfv  5484  eluniimadm  5544  genpassl  7081  genpassu  7082  1idprl  7147  1idpru  7148  axcaucvglemres  7432  negeq0  7734  muleqadd  8135  crap0  8416  addltmul  8650  fzrev  9494  modq0  9732  cjap0  10337  cjne0  10338  caucvgrelemrec  10408  lenegsq  10524  isumss  10779  fsumsplit  10797  sumsplitdc  10822  dvdsabseq  11122  oddennn  11479  elabgf0  11632