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-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:  3bitr4g  222  bibi2i  226  equsalh  1704  eueq3dc  2858  sbcel12g  3017  sbceqg  3018  sbcnel12g  3019  reldisj  3414  r19.3rm  3451  rabxp  4576  elrng  4730  iss  4865  eliniseg  4909  fcnvres  5306  dffv3g  5417  funimass4  5472  fndmdif  5525  fneqeql  5528  funimass3  5536  elrnrexdmb  5560  dff4im  5566  fconst4m  5640  elunirn  5667  riota1  5748  riota2df  5750  f1ocnvfv3  5763  eqfnov  5877  caoftrn  6007  mpoxopovel  6138  rntpos  6154  ordgt0ge1  6332  iinerm  6501  erinxp  6503  qliftfun  6511  mapdm0  6557  elfi2  6860  fifo  6868  inl11  6950  ctssdccl  6996  isomnimap  7009  ismkvmap  7028  pr2nelem  7047  indpi  7150  genpdflem  7315  genpdisj  7331  genpassl  7332  genpassu  7333  ltnqpri  7402  ltpopr  7403  ltexprlemm  7408  ltexprlemdisj  7414  ltexprlemloc  7415  ltrennb  7662  letri3  7845  letr  7847  ltneg  8224  leneg  8227  reapltxor  8351  apsym  8368  suprnubex  8711  suprleubex  8712  elnnnn0  9020  zrevaddcl  9104  znnsub  9105  znn0sub  9119  prime  9150  eluz2  9332  eluz2b1  9395  nn01to3  9409  qrevaddcl  9436  xrletri3  9588  xrletr  9591  iccid  9708  elicopnf  9752  fzsplit2  9830  fzsn  9846  fzpr  9857  uzsplit  9872  fvinim0ffz  10018  lt2sqi  10380  le2sqi  10381  abs00ap  10834  iooinsup  11046  mertenslem2  11305  gcddiv  11707  algcvgblem  11730  isprm3  11799  eltg2b  12223  discld  12305  opnssneib  12325  restbasg  12337  ssidcn  12379  cnptoprest2  12409  lmss  12415  txrest  12445  txlm  12448  imasnopn  12468  bldisj  12570  xmeter  12605  bl2ioo  12711  limcdifap  12800  bj-sseq  12999  nnti  13191