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  7164  eluniima  7254  dfac2b  10209  alephval2  10657  adderpqlem  11039  1idpr  11114  leloe  11396  negeq0  11612  addeq0  11739  muleqadd  11960  addltmul  12582  xrleloe  13273  fzrev  13721  mod0  14016  modirr  14085  cjne0  15330  lenegsq  15488  fsumsplit  15907  sumsplit  15934  dvdsabseq  16483  xpsfrnel  17734  isacs2  17827  acsfn  17833  comfeq  17880  sgrp2nmndlem3  19124  resscntz  19547  gexdvds  19798  hauscmplem  23724  hausdiag  23964  utop3cls  24570  affineequivne  27155  eqcuts2  28172  z12sge0  28869  ltgov  29060  ax5seglem4  29510  mdsl2i  32924  rspc2daf  33105  cycpmco2  33736  cntrval2  33774  pl1cn  34629  fineqvpow  35825  satefvfmla1  36232  bj-isrvec  38258  topdifinfeq  38316  finxpreclem6  38362  wl-sb8ft  38525  ftc1anclem5  38658  findcard4  38675  fdc1  38723  relcnveq  39303  relcnveq2  39304  elrelscnveq  39603  elrelscnveq2  39604  lcvexchlem1  40134  lkreqN  40270  glbconxN  40478  islpln5  40635  islvol5  40679  cdlemefrs29bpre0  41496  cdlemg17h  41768  cdlemg33b  41807  tfsconcat0i  44390  tfsconcat0b  44391  oadif1lem  44424  oadif1  44425  brnonrel  44632  frege92  44998  e2ebind  45589  stoweidlem28  47081  clnbupgrel  48975  0funcg2  50235