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  2516  necon2bbid  2982  notzfaus  5369  fressnfv  7180  eluniima  7270  dfac2b  10169  alephval2  10610  adderpqlem  10992  1idpr  11067  leloe  11345  negeq0  11561  addeq0  11684  muleqadd  11905  addltmul  12500  xrleloe  13183  fzrev  13624  mod0  13913  modirr  13980  cjne0  15199  lenegsq  15356  fsumsplit  15774  sumsplit  15801  dvdsabseq  16347  xpsfrnel  17609  isacs2  17698  acsfn  17704  comfeq  17751  sgrp2nmndlem3  18951  resscntz  19364  gexdvds  19617  hauscmplem  23430  hausdiag  23669  utop3cls  24276  affineequivne  26885  eqscut2  27866  ltgov  28620  ax5seglem4  28962  mdsl2i  32351  rspc2daf  32495  cycpmco2  33136  pl1cn  33916  fineqvpow  35089  satefvfmla1  35410  bj-isrvec  37277  topdifinfeq  37333  finxpreclem6  37379  wl-sb8ft  37531  ftc1anclem5  37684  fdc1  37733  relcnveq  38304  relcnveq2  38305  elrelscnveq  38474  elrelscnveq2  38475  lcvexchlem1  39016  lkreqN  39152  glbconxN  39361  islpln5  39518  islvol5  39562  cdlemefrs29bpre0  40379  cdlemg17h  40651  cdlemg33b  40690  tfsconcat0i  43335  tfsconcat0b  43336  oadif1lem  43369  oadif1  43370  brnonrel  43579  frege92  43945  e2ebind  44561  stoweidlem28  45984  clnbupgrel  47759