Theorem bitr3di 286

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 224	. 2 ⊢ (𝜃 ↔ 𝜓)
3		bitr3di.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	bitr2id 284	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbco3  2518  necon2bbid  2976  notzfaus  5298  fressnfv  7105  eluniima  7196  dfac2b  10042  alephval2  10484  adderpqlem  10866  1idpr  10941  leloe  11220  negeq0  11436  addeq0  11561  muleqadd  11782  addltmul  12378  xrleloe  13059  fzrev  13504  mod0  13797  modirr  13866  cjne0  15087  lenegsq  15245  fsumsplit  15665  sumsplit  15692  dvdsabseq  16241  xpsfrnel  17484  isacs2  17577  acsfn  17583  comfeq  17630  sgrp2nmndlem3  18854  resscntz  19266  gexdvds  19517  hauscmplem  23349  hausdiag  23588  utop3cls  24194  affineequivne  26777  eqcuts2  27766  z12sge0  28463  ltgov  28653  ax5seglem4  28989  mdsl2i  32382  rspc2daf  32524  cycpmco2  33199  cntrval2  33237  pl1cn  34105  fineqvpow  35265  satefvfmla1  35613  bj-isrvec  37606  topdifinfeq  37662  finxpreclem6  37708  wl-sb8ft  37866  ftc1anclem5  38009  fdc1  38058  relcnveq  38640  relcnveq2  38641  elrelscnveq  38940  elrelscnveq2  38941  lcvexchlem1  39471  lkreqN  39607  glbconxN  39815  islpln5  39972  islvol5  40016  cdlemefrs29bpre0  40833  cdlemg17h  41105  cdlemg33b  41144  tfsconcat0i  43776  tfsconcat0b  43777  oadif1lem  43810  oadif1  43811  brnonrel  44019  frege92  44385  e2ebind  44993  stoweidlem28  46460  clnbupgrel  48268  0funcg2  49517