Theorem syl6bbr 197

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		syl6bbr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	bicomi 131	. 2 ⊢ (𝜒 ↔ 𝜃)
4	1, 3	syl6bb 195	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:  3bitr4g  222  bibi2i  226  equsalh  1672  eueq3dc  2811  sbcel12g  2968  sbceqg  2969  sbcnel12g  2970  reldisj  3361  r19.3rm  3398  rabxp  4514  elrng  4668  iss  4801  eliniseg  4845  fcnvres  5242  dffv3g  5349  funimass4  5404  fndmdif  5457  fneqeql  5460  funimass3  5468  elrnrexdmb  5492  dff4im  5498  fconst4m  5572  elunirn  5599  riota1  5680  riota2df  5682  f1ocnvfv3  5695  eqfnov  5809  caoftrn  5938  mpoxopovel  6068  rntpos  6084  ordgt0ge1  6262  iinerm  6431  erinxp  6433  qliftfun  6441  mapdm0  6487  inl11  6865  ctssdclemr  6911  isomnimap  6921  ismkvmap  6940  pr2nelem  6958  indpi  7051  genpdflem  7216  genpdisj  7232  genpassl  7233  genpassu  7234  ltnqpri  7303  ltpopr  7304  ltexprlemm  7309  ltexprlemdisj  7315  ltexprlemloc  7316  ltrennb  7541  letri3  7716  letr  7718  ltneg  8091  leneg  8094  reapltxor  8217  apsym  8234  suprnubex  8569  suprleubex  8570  elnnnn0  8872  zrevaddcl  8956  znnsub  8957  znn0sub  8971  prime  9002  eluz2  9182  eluz2b1  9245  nn01to3  9259  qrevaddcl  9286  xrletri3  9429  xrletr  9432  iccid  9549  elicopnf  9593  fzsplit2  9671  fzsn  9687  fzpr  9698  uzsplit  9713  fvinim0ffz  9859  lt2sqi  10221  le2sqi  10222  abs00ap  10674  iooinsup  10885  mertenslem2  11144  gcddiv  11500  algcvgblem  11523  isprm3  11592  eltg2b  12005  discld  12087  opnssneib  12107  restbasg  12119  ssidcn  12160  cnptoprest2  12190  lmss  12196  txrest  12226  txlm  12229  imasnopn  12249  bldisj  12329  xmeter  12364  bl2ioo  12461  limcdifap  12512  bj-sseq  12580  nnti  12776