Theorem bitr3di 288

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  sbco3  2545  necon2bbid  3001  notzfaus  5321  fressnfv  7143  eluniima  7234  dfac2b  10098  alephval2  10541  adderpqlem  10923  1idpr  10998  leloe  11280  negeq0  11496  addeq0  11621  muleqadd  11842  addltmul  12467  xrleloe  13156  fzrev  13602  mod0  13896  modirr  13965  cjne0  15200  lenegsq  15358  fsumsplit  15778  sumsplit  15805  dvdsabseq  16357  xpsfrnel  17602  isacs2  17695  acsfn  17701  comfeq  17748  sgrp2nmndlem3  18972  resscntz  19383  gexdvds  19634  hauscmplem  23473  hausdiag  23712  utop3cls  24318  affineequivne  26899  eqcuts2  27886  z12sge0  28583  ltgov  28773  ax5seglem4  29140  mdsl2i  32532  rspc2daf  32672  cycpmco2  33319  cntrval2  33357  pl1cn  34254  fineqvpow  35415  satefvfmla1  35780  bj-isrvec  37791  topdifinfeq  37849  finxpreclem6  37895  wl-sb8ft  38058  ftc1anclem5  38201  fdc1  38250  relcnveq  38832  relcnveq2  38833  elrelscnveq  39132  elrelscnveq2  39133  lcvexchlem1  39663  lkreqN  39799  glbconxN  40007  islpln5  40164  islvol5  40208  cdlemefrs29bpre0  41025  cdlemg17h  41297  cdlemg33b  41336  tfsconcat0i  43927  tfsconcat0b  43928  oadif1lem  43961  oadif1  43962  brnonrel  44170  frege92  44536  e2ebind  45130  stoweidlem28  46593  clnbupgrel  48447  0funcg2  49696