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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbco3  2515  necon2bbid  2985  notzfaus  5294  fressnfv  7064  eluniima  7155  dfac2b  9936  alephval2  10378  adderpqlem  10760  1idpr  10835  leloe  11111  negeq0  11325  addeq0  11448  muleqadd  11669  addltmul  12259  xrleloe  12928  fzrev  13369  mod0  13646  modirr  13712  cjne0  14923  lenegsq  15081  fsumsplit  15502  sumsplit  15529  dvdsabseq  16071  xpsfrnel  17322  isacs2  17411  acsfn  17417  comfeq  17464  sgrp2nmndlem3  18613  resscntz  18987  gexdvds  19238  hauscmplem  22606  hausdiag  22845  utop3cls  23452  affineequivne  26026  ltgov  27007  ax5seglem4  27349  mdsl2i  30733  rspc2daf  30865  cycpmco2  31449  pl1cn  31954  fineqvpow  33114  satefvfmla1  33436  eqscut2  34049  bj-isrvec  35513  topdifinfeq  35569  finxpreclem6  35615  ftc1anclem5  35902  fdc1  35952  relcnveq  36535  relcnveq2  36536  elrelscnveq  36706  elrelscnveq2  36707  lcvexchlem1  37248  lkreqN  37384  glbconxN  37592  islpln5  37749  islvol5  37793  cdlemefrs29bpre0  38610  cdlemg17h  38882  cdlemg33b  38921  brnonrel  41410  frege92  41776  e2ebind  42396  stoweidlem28  43798