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  2515  necon2bbid  2973  notzfaus  5305  fressnfv  7102  eluniima  7193  dfac2b  10032  alephval2  10473  adderpqlem  10855  1idpr  10930  leloe  11209  negeq0  11425  addeq0  11550  muleqadd  11771  addltmul  12367  xrleloe  13053  fzrev  13497  mod0  13790  modirr  13859  cjne0  15080  lenegsq  15238  fsumsplit  15658  sumsplit  15685  dvdsabseq  16234  xpsfrnel  17476  isacs2  17569  acsfn  17575  comfeq  17622  sgrp2nmndlem3  18843  resscntz  19255  gexdvds  19506  hauscmplem  23331  hausdiag  23570  utop3cls  24176  affineequivne  26774  eqscut2  27757  zs12ge0  28403  ltgov  28585  ax5seglem4  28921  mdsl2i  32313  rspc2daf  32456  cycpmco2  33113  cntrval2  33151  pl1cn  33979  fineqvpow  35149  satefvfmla1  35480  bj-isrvec  37349  topdifinfeq  37405  finxpreclem6  37451  wl-sb8ft  37605  ftc1anclem5  37747  fdc1  37796  relcnveq  38370  relcnveq2  38371  elrelscnveq  38650  elrelscnveq2  38651  lcvexchlem1  39143  lkreqN  39279  glbconxN  39487  islpln5  39644  islvol5  39688  cdlemefrs29bpre0  40505  cdlemg17h  40777  cdlemg33b  40816  tfsconcat0i  43452  tfsconcat0b  43453  oadif1lem  43486  oadif1  43487  brnonrel  43696  frege92  44062  e2ebind  44670  stoweidlem28  46140  clnbupgrel  47948  0funcg2  49199