Theorem syl5rbbr 184

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 123	. 2 ⊢ (𝜑 ↔ 𝜓)
3		syl5rbbr.2	. 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
4	2, 3	syl5rbb 182	1 ⊢ (𝜒 → (𝜃 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  xordc  1283  sbal2  1898  eqsnm  3526  fnressn  5349  fressnfv  5350  eluniimadm  5404  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  axcaucvglemres  6973  negeq0  7265  muleqadd  7649  crap0  7910  addltmul  8161  fzrev  8946  modq0  9171  cjap0  9507  cjne0  9508  caucvgrelemrec  9578  lenegsq  9691  elabgf0  9916