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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sbco3  2504  necon2bbid  2976  notzfaus  5351  fressnfv  7150  eluniima  7241  dfac2b  10120  alephval2  10562  adderpqlem  10944  1idpr  11019  leloe  11296  negeq0  11510  addeq0  11633  muleqadd  11854  addltmul  12444  xrleloe  13119  fzrev  13560  mod0  13837  modirr  13903  cjne0  15106  lenegsq  15263  fsumsplit  15683  sumsplit  15710  dvdsabseq  16252  xpsfrnel  17504  isacs2  17593  acsfn  17599  comfeq  17646  sgrp2nmndlem3  18837  resscntz  19234  gexdvds  19489  hauscmplem  23220  hausdiag  23459  utop3cls  24066  affineequivne  26663  eqscut2  27643  ltgov  28272  ax5seglem4  28614  mdsl2i  31999  rspc2daf  32132  cycpmco2  32719  pl1cn  33390  fineqvpow  34551  satefvfmla1  34871  bj-isrvec  36631  topdifinfeq  36687  finxpreclem6  36733  ftc1anclem5  37021  fdc1  37070  relcnveq  37647  relcnveq2  37648  elrelscnveq  37818  elrelscnveq2  37819  lcvexchlem1  38360  lkreqN  38496  glbconxN  38705  islpln5  38862  islvol5  38906  cdlemefrs29bpre0  39723  cdlemg17h  39995  cdlemg33b  40034  tfsconcat0i  42550  tfsconcat0b  42551  oadif1lem  42584  oadif1  42585  brnonrel  42795  frege92  43161  e2ebind  43779  stoweidlem28  45195