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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  xordc  1329  sbal2  1947  eqsnm  3605  fnressn  5497  fressnfv  5498  eluniimadm  5558  genpassl  7144  genpassu  7145  1idprl  7210  1idpru  7211  axcaucvglemres  7495  negeq0  7797  muleqadd  8198  crap0  8479  addltmul  8713  fzrev  9559  modq0  9797  cjap0  10402  cjne0  10403  caucvgrelemrec  10473  lenegsq  10589  isumss  10844  fsumsplit  10862  sumsplitdc  10887  dvdsabseq  11187  oddennn  11544  elabgf0  11950