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  6202  sbcoteq1a  7998  fnwelem  8075  mpocurryd  8213  compssiso  10290  divfl0  13777  cjreb  15079  cnpart  15196  bitsuz  16437  acsfn  17619  eqg0el  19152  ghmeqker  19212  odmulg  19525  psrbaglefi  21919  cnrest2  23264  hausdiag  23623  prdsbl  24469  mcubic  26827  2lgslem1a2  27370  fmptco1f1o  32724  qsidomlem2  33531  areacirclem4  38049  lmclim2  38096  cmtbr2N  39716  expdiophlem1  43470  cantnfresb  43773  rrx2linest  49233