Theorem syl6rbbr 198

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 131	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6rbb 196	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:  imimorbdc  834  baib  867  pm5.6dc  874  xornbidc  1328  mo2dc  2004  reu8  2812  sbc6g  2865  dfss4st  3233  r19.28m  3375  r19.45mv  3379  r19.44mv  3380  r19.27m  3381  ralsnsg  3484  ralsns  3485  iunconstm  3744  iinconstm  3745  unisucg  4250  relsng  4554  funssres  5069  fncnv  5093  dff1o5  5275  funimass4  5368  fneqeql2  5422  fnniniseg2  5436  rexsupp  5437  unpreima  5438  dffo3  5460  funfvima  5540  dff13  5561  f1eqcocnv  5584  fliftf  5592  isocnv2  5605  eloprabga  5749  mpt22eqb  5768  opabex3d  5906  opabex3  5907  elxp6  5954  elxp7  5955  sbthlemi5  6724  sbthlemi6  6725  genpdflem  7127  ltnqpr  7213  ltexprlemloc  7227  xrlenlt  7612  negcon2  7796  dfinfre  8478  elznn  8827  zq  9172  rpnegap  9227  modqmuladdnn0  9836  shftdm  10317  rexfiuz  10483  rexanuz2  10485  sumsplitdc  10887  fsum2dlemstep  10889  odd2np1  11212  divalgb  11264  infssuzex  11284  isprm4  11440