Theorem syl6rbbr 197

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
syl6rbbr.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
syl6rbbr.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
syl6rbbr	⊢ (𝜑 → (𝜃 ↔ 𝜓))

Proof of Theorem syl6rbbr

Step	Hyp	Ref	Expression
1		syl6rbbr.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6rbbr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 130	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6rbb 195	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:  imimorbdc  828  baib  861  pm5.6dc  868  xornbidc  1322  mo2dc  1996  reu8  2788  sbc6g  2839  r19.28m  3331  r19.45mv  3335  r19.27m  3336  ralsnsg  3430  ralsns  3431  iunconstm  3686  iinconstm  3687  unisucg  4169  funssres  4962  fncnv  4985  dff1o5  5155  funimass4  5245  fneqeql2  5297  fnniniseg2  5311  rexsupp  5312  unpreima  5313  dffo3  5335  funfvima  5411  dff13  5428  f1eqcocnv  5451  fliftf  5459  isocnv2  5472  eloprabga  5611  mpt22eqb  5630  opabex3d  5768  opabex3  5769  elxp6  5816  elxp7  5817  genpdflem  6697  ltnqpr  6783  ltexprlemloc  6797  xrlenlt  7177  negcon2  7361  dfinfre  8034  elznn  8367  zq  8711  rpnegap  8766  modqmuladdnn0  9370  shftdm  9710  rexfiuz  9875  rexanuz2  9877  odd2np1  10272  divalgb  10325  infssuzex  10345  isprm4  10501