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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imimorbdc  881  baib  904  pm5.6dc  911  xornbidc  1369  mo2dc  2054  reu8  2880  sbc6g  2933  dfss4st  3309  r19.28m  3452  r19.45mv  3456  r19.44mv  3457  r19.27m  3458  ralsnsg  3561  ralsns  3562  iunconstm  3821  iinconstm  3822  exmidsssnc  4126  unisucg  4336  relsng  4642  funssres  5165  fncnv  5189  dff1o5  5376  funimass4  5472  fneqeql2  5529  fnniniseg2  5543  rexsupp  5544  unpreima  5545  dffo3  5567  funfvima  5649  dff13  5669  f1eqcocnv  5692  fliftf  5700  isocnv2  5713  eloprabga  5858  mpo2eqb  5880  opabex3d  6019  opabex3  6020  elxp6  6067  elxp7  6068  sbthlemi5  6849  sbthlemi6  6850  genpdflem  7315  ltnqpr  7401  ltexprlemloc  7415  xrlenlt  7829  negcon2  8015  dfinfre  8714  sup3exmid  8715  elznn  9070  zq  9418  rpnegap  9474  modqmuladdnn0  10141  shftdm  10594  rexfiuz  10761  rexanuz2  10763  sumsplitdc  11201  fsum2dlemstep  11203  odd2np1  11570  divalgb  11622  infssuzex  11642  isprm4  11800  ctiunctlemudc  11950  tx1cn  12438  tx2cn  12439  cnbl0  12703  cnblcld  12704  reopnap  12707  pilem1  12860  sinq34lt0t  12912