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  6263  sbcoteq1a  8076  fnwelem  8156  mpocurryd  8294  compssiso  10414  divfl0  13864  cjreb  15162  cnpart  15279  bitsuz  16511  acsfn  17702  eqg0el  19201  ghmeqker  19261  odmulg  19574  psrbaglefi  21946  cnrest2  23294  hausdiag  23653  prdsbl  24504  mcubic  26890  2lgslem1a2  27434  fmptco1f1o  32643  qsidomlem2  33481  areacirclem4  37718  lmclim2  37765  cmtbr2N  39254  expdiophlem1  43033  cantnfresb  43337  rrx2linest  48663