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	syl5rbb 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  2533  necon2bbid  2992  notzfaus  5223  fressnfv  6906  eluniima  6994  dfac2b  9575  alephval2  10017  adderpqlem  10399  1idpr  10474  leloe  10750  negeq0  10963  addeq0  11086  muleqadd  11307  addltmul  11895  xrleloe  12563  fzrev  13004  mod0  13278  modirr  13344  cjne0  14555  lenegsq  14713  fsumsplit  15130  sumsplit  15156  dvdsabseq  15699  xpsfrnel  16878  isacs2  16967  acsfn  16973  comfeq  17019  sgrp2nmndlem3  18141  resscntz  18514  gexdvds  18761  hauscmplem  22091  hausdiag  22330  utop3cls  22937  affineequivne  25497  ltgov  26475  ax5seglem4  26810  mdsl2i  30189  rspc2daf  30322  cycpmco2  30911  pl1cn  31411  satefvfmla1  32888  eqscut2  33546  topdifinfeq  35032  finxpreclem6  35078  ftc1anclem5  35399  fdc1  35449  relcnveq  36004  relcnveq2  36005  elrelscnveq  36157  elrelscnveq2  36158  lcvexchlem1  36595  lkreqN  36731  glbconxN  36939  islpln5  37096  islvol5  37140  cdlemefrs29bpre0  37957  cdlemg17h  38229  cdlemg33b  38268  brnonrel  40647  frege92  41014  e2ebind  41627  stoweidlem28  43021