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  2521  necon2bbid  2990  notzfaus  5381  fressnfv  7194  eluniima  7287  dfac2b  10200  alephval2  10641  adderpqlem  11023  1idpr  11098  leloe  11376  negeq0  11590  addeq0  11713  muleqadd  11934  addltmul  12529  xrleloe  13206  fzrev  13647  mod0  13927  modirr  13993  cjne0  15212  lenegsq  15369  fsumsplit  15789  sumsplit  15816  dvdsabseq  16361  xpsfrnel  17622  isacs2  17711  acsfn  17717  comfeq  17764  sgrp2nmndlem3  18960  resscntz  19373  gexdvds  19626  hauscmplem  23435  hausdiag  23674  utop3cls  24281  affineequivne  26888  eqscut2  27869  ltgov  28623  ax5seglem4  28965  mdsl2i  32354  rspc2daf  32495  cycpmco2  33126  pl1cn  33901  fineqvpow  35072  satefvfmla1  35393  bj-isrvec  37260  topdifinfeq  37316  finxpreclem6  37362  wl-sb8ft  37504  ftc1anclem5  37657  fdc1  37706  relcnveq  38278  relcnveq2  38279  elrelscnveq  38448  elrelscnveq2  38449  lcvexchlem1  38990  lkreqN  39126  glbconxN  39335  islpln5  39492  islvol5  39536  cdlemefrs29bpre0  40353  cdlemg17h  40625  cdlemg33b  40664  tfsconcat0i  43307  tfsconcat0b  43308  oadif1lem  43341  oadif1  43342  brnonrel  43551  frege92  43917  e2ebind  44534  stoweidlem28  45949  clnbupgrel  47707