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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  sbco3  2511  necon2bbid  2968  notzfaus  5318  fressnfv  7132  eluniima  7224  dfac2b  10084  alephval2  10525  adderpqlem  10907  1idpr  10982  leloe  11260  negeq0  11476  addeq0  11601  muleqadd  11822  addltmul  12418  xrleloe  13104  fzrev  13548  mod0  13838  modirr  13907  cjne0  15129  lenegsq  15287  fsumsplit  15707  sumsplit  15734  dvdsabseq  16283  xpsfrnel  17525  isacs2  17614  acsfn  17620  comfeq  17667  sgrp2nmndlem3  18852  resscntz  19265  gexdvds  19514  hauscmplem  23293  hausdiag  23532  utop3cls  24139  affineequivne  26737  eqscut2  27718  zs12ge0  28342  ltgov  28524  ax5seglem4  28859  mdsl2i  32251  rspc2daf  32395  cycpmco2  33090  cntrval2  33128  pl1cn  33945  fineqvpow  35086  satefvfmla1  35412  bj-isrvec  37282  topdifinfeq  37338  finxpreclem6  37384  wl-sb8ft  37538  ftc1anclem5  37691  fdc1  37740  relcnveq  38310  relcnveq2  38311  elrelscnveq  38483  elrelscnveq2  38484  lcvexchlem1  39027  lkreqN  39163  glbconxN  39372  islpln5  39529  islvol5  39573  cdlemefrs29bpre0  40390  cdlemg17h  40662  cdlemg33b  40701  tfsconcat0i  43334  tfsconcat0b  43335  oadif1lem  43368  oadif1  43369  brnonrel  43578  frege92  43944  e2ebind  44553  stoweidlem28  46026  clnbupgrel  47835  0funcg2  49073