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	bitr2id 287	1 ⊢ (𝜑 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbco3  2542  necon2bbid  2998  notsep  5324  fressnfv  7152  eluniima  7242  dfac2b  10180  alephval2  10628  adderpqlem  11010  1idpr  11085  leloe  11367  negeq0  11583  addeq0  11708  muleqadd  11929  addltmul  12551  xrleloe  13242  fzrev  13689  mod0  13984  modirr  14053  cjne0  15297  lenegsq  15455  fsumsplit  15874  sumsplit  15901  dvdsabseq  16450  xpsfrnel  17695  isacs2  17788  acsfn  17794  comfeq  17841  sgrp2nmndlem3  19085  resscntz  19508  gexdvds  19759  hauscmplem  23685  hausdiag  23925  utop3cls  24531  affineequivne  27118  eqcuts2  28105  z12sge0  28802  ltgov  28993  ax5seglem4  29443  mdsl2i  32857  rspc2daf  32996  cycpmco2  33627  cntrval2  33665  pl1cn  34520  fineqvpow  35708  satefvfmla1  36111  bj-isrvec  38135  topdifinfeq  38193  finxpreclem6  38239  wl-sb8ft  38402  ftc1anclem5  38535  findcard4  38552  fdc1  38600  relcnveq  39180  relcnveq2  39181  elrelscnveq  39480  elrelscnveq2  39481  lcvexchlem1  40011  lkreqN  40147  glbconxN  40355  islpln5  40512  islvol5  40556  cdlemefrs29bpre0  41373  cdlemg17h  41645  cdlemg33b  41684  tfsconcat0i  44290  tfsconcat0b  44291  oadif1lem  44324  oadif1  44325  brnonrel  44533  frege92  44899  e2ebind  45490  stoweidlem28  46960  clnbupgrel  48854  0funcg2  50114