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  6192  sbcoteq1a  7986  fnwelem  8064  mpocurryd  8202  compssiso  10268  divfl0  13728  cjreb  15030  cnpart  15147  bitsuz  16385  acsfn  17565  eqg0el  19062  ghmeqker  19122  odmulg  19435  psrbaglefi  21833  cnrest2  23171  hausdiag  23530  prdsbl  24377  mcubic  26755  2lgslem1a2  27299  fmptco1f1o  32576  qsidomlem2  33390  areacirclem4  37691  lmclim2  37738  cmtbr2N  39232  expdiophlem1  42994  cantnfresb  43297  rrx2linest  48727