Theorem 3bitrrd 309

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitrd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))
3bitrd.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitrrd	⊢ (𝜑 → (𝜏 ↔ 𝜓))

Proof of Theorem 3bitrrd

Step	Hyp	Ref	Expression
1		3bitrd.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
2		3bitrd.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3bitrd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	2, 3	bitr2d 283	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	1, 4	bitr3d 284	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:  rnmpt0f  6247  sbcoteq1a  8066  fnwelem  8149  mpocurryd  8293  compssiso  10459  divfl0  13971  cjreb  15299  cnpart  15416  bitsuz  16653  acsfn  17842  eqg0el  19407  ghmeqker  19466  odmulg  19779  qsidomlem2  21646  psrbaglefi  22243  cnrest2  23613  hausdiag  23973  prdsbl  24819  mcubic  27184  2lgslem1a2  27726  fmptco1f1o  33278  areacirclem4  38738  lmclim2  38801  cmtbr2N  40419  expdiophlem1  44137  cantnfresb  44435  rrx2linest  49962