Theorem bitr3di 285

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 283	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  2510  necon2bbid  2982  notzfaus  5360  fressnfv  7159  eluniima  7251  dfac2b  10127  alephval2  10569  adderpqlem  10951  1idpr  11026  leloe  11304  negeq0  11518  addeq0  11641  muleqadd  11862  addltmul  12452  xrleloe  13127  fzrev  13568  mod0  13845  modirr  13911  cjne0  15114  lenegsq  15271  fsumsplit  15691  sumsplit  15718  dvdsabseq  16260  xpsfrnel  17512  isacs2  17601  acsfn  17607  comfeq  17654  sgrp2nmndlem3  18842  resscntz  19238  gexdvds  19493  hauscmplem  23130  hausdiag  23369  utop3cls  23976  affineequivne  26568  eqscut2  27544  ltgov  28115  ax5seglem4  28457  mdsl2i  31842  rspc2daf  31975  cycpmco2  32562  pl1cn  33233  fineqvpow  34394  satefvfmla1  34714  bj-isrvec  36478  topdifinfeq  36534  finxpreclem6  36580  ftc1anclem5  36868  fdc1  36917  relcnveq  37494  relcnveq2  37495  elrelscnveq  37665  elrelscnveq2  37666  lcvexchlem1  38207  lkreqN  38343  glbconxN  38552  islpln5  38709  islvol5  38753  cdlemefrs29bpre0  39570  cdlemg17h  39842  cdlemg33b  39881  tfsconcat0i  42397  tfsconcat0b  42398  oadif1lem  42431  oadif1  42432  brnonrel  42642  frege92  43008  e2ebind  43626  stoweidlem28  45042