Theorem bitr3di 288

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
bitr3di	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Proof of Theorem bitr3di

Step	Hyp	Ref	Expression
1		bitr3di.2	. . 3 ⊢ (𝜓 ↔ 𝜃)
2	1	bicomi 226	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 286	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  sbco3  2534  necon2bbid  2990  notzfaus  5310  fressnfv  7128  eluniima  7219  dfac2b  10073  alephval2  10516  adderpqlem  10898  1idpr  10973  leloe  11255  negeq0  11471  addeq0  11596  muleqadd  11817  addltmul  12443  xrleloe  13132  fzrev  13578  mod0  13872  modirr  13941  cjne0  15162  lenegsq  15320  fsumsplit  15740  sumsplit  15767  dvdsabseq  16319  xpsfrnel  17564  isacs2  17657  acsfn  17663  comfeq  17710  sgrp2nmndlem3  18934  resscntz  19345  gexdvds  19596  hauscmplem  23435  hausdiag  23674  utop3cls  24280  affineequivne  26858  eqcuts2  27845  z12sge0  28542  ltgov  28732  ax5seglem4  29068  mdsl2i  32460  rspc2daf  32602  cycpmco2  33263  cntrval2  33301  pl1cn  34196  fineqvpow  35356  satefvfmla1  35713  bj-isrvec  37724  topdifinfeq  37782  finxpreclem6  37828  wl-sb8ft  37991  ftc1anclem5  38134  fdc1  38183  relcnveq  38765  relcnveq2  38766  elrelscnveq  39065  elrelscnveq2  39066  lcvexchlem1  39596  lkreqN  39732  glbconxN  39940  islpln5  40097  islvol5  40141  cdlemefrs29bpre0  40958  cdlemg17h  41230  cdlemg33b  41269  tfsconcat0i  43860  tfsconcat0b  43861  oadif1lem  43894  oadif1  43895  brnonrel  44103  frege92  44469  e2ebind  45077  stoweidlem28  46540  clnbupgrel  48394  0funcg2  49643