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 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rnmpt0f  6245  sbcoteq1a  8047  fnwelem  8126  mpocurryd  8264  compssiso  10357  divfl0  13856  cjreb  15173  cnpart  15290  bitsuz  16531  acsfn  17714  eqg0el  19253  ghmeqker  19312  odmulg  19625  qsidomlem2  21449  psrbaglefi  22044  cnrest2  23411  hausdiag  23770  prdsbl  24616  mcubic  26977  2lgslem1a2  27519  fmptco1f1o  32918  areacirclem4  38249  lmclim2  38296  cmtbr2N  39916  expdiophlem1  43639  cantnfresb  43942  rrx2linest  49406