Theorem 3bitrrd 306

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 280	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	1, 4	bitr3d 281	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:  rnmpt0f  6207  sbcoteq1a  8004  fnwelem  8081  mpocurryd  8219  compssiso  10296  divfl0  13783  cjreb  15085  cnpart  15202  bitsuz  16443  acsfn  17625  eqg0el  19158  ghmeqker  19218  odmulg  19531  psrbaglefi  21906  cnrest2  23251  hausdiag  23610  prdsbl  24456  mcubic  26811  2lgslem1a2  27353  fmptco1f1o  32706  qsidomlem2  33513  areacirclem4  38032  lmclim2  38079  cmtbr2N  39699  expdiophlem1  43449  cantnfresb  43752  rrx2linest  49218