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  5306  fressnfv  7114  eluniima  7205  dfac2b  10053  alephval2  10495  adderpqlem  10877  1idpr  10952  leloe  11232  negeq0  11448  addeq0  11573  muleqadd  11794  addltmul  12413  xrleloe  13095  fzrev  13541  mod0  13835  modirr  13904  cjne0  15125  lenegsq  15283  fsumsplit  15703  sumsplit  15730  dvdsabseq  16282  xpsfrnel  17526  isacs2  17619  acsfn  17625  comfeq  17672  sgrp2nmndlem3  18896  resscntz  19308  gexdvds  19559  hauscmplem  23371  hausdiag  23610  utop3cls  24216  affineequivne  26791  eqcuts2  27778  z12sge0  28475  ltgov  28665  ax5seglem4  29001  mdsl2i  32393  rspc2daf  32535  cycpmco2  33194  cntrval2  33232  pl1cn  34099  fineqvpow  35259  satefvfmla1  35607  bj-isrvec  37608  topdifinfeq  37666  finxpreclem6  37712  wl-sb8ft  37875  ftc1anclem5  38018  fdc1  38067  relcnveq  38649  relcnveq2  38650  elrelscnveq  38949  elrelscnveq2  38950  lcvexchlem1  39480  lkreqN  39616  glbconxN  39824  islpln5  39981  islvol5  40025  cdlemefrs29bpre0  40842  cdlemg17h  41114  cdlemg33b  41153  tfsconcat0i  43773  tfsconcat0b  43774  oadif1lem  43807  oadif1  43808  brnonrel  44016  frege92  44382  e2ebind  44990  stoweidlem28  46456  clnbupgrel  48304  0funcg2  49553