Theorem bitr3di 289

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbco3  2516  necon2bbid  2984  notzfaus  5254  fressnfv  6975  eluniima  7063  dfac2b  9744  alephval2  10186  adderpqlem  10568  1idpr  10643  leloe  10919  negeq0  11132  addeq0  11255  muleqadd  11476  addltmul  12066  xrleloe  12734  fzrev  13175  mod0  13449  modirr  13515  cjne0  14726  lenegsq  14884  fsumsplit  15305  sumsplit  15332  dvdsabseq  15874  xpsfrnel  17067  isacs2  17156  acsfn  17162  comfeq  17209  sgrp2nmndlem3  18352  resscntz  18726  gexdvds  18973  hauscmplem  22303  hausdiag  22542  utop3cls  23149  affineequivne  25710  ltgov  26688  ax5seglem4  27023  mdsl2i  30403  rspc2daf  30535  cycpmco2  31119  pl1cn  31619  fineqvpow  32778  satefvfmla1  33100  eqscut2  33737  topdifinfeq  35258  finxpreclem6  35304  ftc1anclem5  35591  fdc1  35641  relcnveq  36194  relcnveq2  36195  elrelscnveq  36347  elrelscnveq2  36348  lcvexchlem1  36785  lkreqN  36921  glbconxN  37129  islpln5  37286  islvol5  37330  cdlemefrs29bpre0  38147  cdlemg17h  38419  cdlemg33b  38458  brnonrel  40873  frege92  41240  e2ebind  41856  stoweidlem28  43244