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  1705  eueq3dc  2862  sbcel12g  3022  sbceqg  3023  sbcnel12g  3024  reldisj  3419  r19.3rm  3456  eldifpr  3559  eldiftp  3577  rabxp  4584  elrng  4738  iss  4873  eliniseg  4917  fcnvres  5314  dffv3g  5425  funimass4  5480  fndmdif  5533  fneqeql  5536  funimass3  5544  elrnrexdmb  5568  dff4im  5574  fconst4m  5648  elunirn  5675  riota1  5756  riota2df  5758  f1ocnvfv3  5771  eqfnov  5885  caoftrn  6015  mpoxopovel  6146  rntpos  6162  ordgt0ge1  6340  iinerm  6509  erinxp  6511  qliftfun  6519  mapdm0  6565  elfi2  6868  fifo  6876  inl11  6958  ctssdccl  7004  isomnimap  7017  ismkvmap  7036  iswomnimap  7048  omniwomnimkv  7049  pr2nelem  7064  indpi  7174  genpdflem  7339  genpdisj  7355  genpassl  7356  genpassu  7357  ltnqpri  7426  ltpopr  7427  ltexprlemm  7432  ltexprlemdisj  7438  ltexprlemloc  7439  ltrennb  7686  letri3  7869  letr  7871  ltneg  8248  leneg  8251  reapltxor  8375  apsym  8392  suprnubex  8735  suprleubex  8736  elnnnn0  9044  zrevaddcl  9128  znnsub  9129  znn0sub  9143  prime  9174  eluz2  9356  eluz2b1  9422  nn01to3  9436  qrevaddcl  9463  xrletri3  9618  xrletr  9621  iccid  9738  elicopnf  9782  fzsplit2  9861  fzsn  9877  fzpr  9888  uzsplit  9903  fvinim0ffz  10049  lt2sqi  10411  le2sqi  10412  abs00ap  10866  iooinsup  11078  mertenslem2  11337  gcddiv  11743  algcvgblem  11766  isprm3  11835  eltg2b  12262  discld  12344  opnssneib  12364  restbasg  12376  ssidcn  12418  cnptoprest2  12448  lmss  12454  txrest  12484  txlm  12487  imasnopn  12507  bldisj  12609  xmeter  12644  bl2ioo  12750  limcdifap  12839  bj-sseq  13170  nnti  13362  pw1nct  13371