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  2052  reu8  2875  sbc6g  2928  dfss4st  3304  r19.28m  3447  r19.45mv  3451  r19.44mv  3452  r19.27m  3453  ralsnsg  3556  ralsns  3557  iunconstm  3816  iinconstm  3817  exmidsssnc  4121  unisucg  4331  relsng  4637  funssres  5160  fncnv  5184  dff1o5  5369  funimass4  5465  fneqeql2  5522  fnniniseg2  5536  rexsupp  5537  unpreima  5538  dffo3  5560  funfvima  5642  dff13  5662  f1eqcocnv  5685  fliftf  5693  isocnv2  5706  eloprabga  5851  mpo2eqb  5873  opabex3d  6012  opabex3  6013  elxp6  6060  elxp7  6061  sbthlemi5  6842  sbthlemi6  6843  genpdflem  7308  ltnqpr  7394  ltexprlemloc  7408  xrlenlt  7822  negcon2  8008  dfinfre  8707  sup3exmid  8708  elznn  9063  zq  9411  rpnegap  9467  modqmuladdnn0  10134  shftdm  10587  rexfiuz  10754  rexanuz2  10756  sumsplitdc  11194  fsum2dlemstep  11196  odd2np1  11559  divalgb  11611  infssuzex  11631  isprm4  11789  ctiunctlemudc  11939  tx1cn  12427  tx2cn  12428  cnbl0  12692  cnblcld  12693  reopnap  12696  pilem1  12849  sinq34lt0t  12901