Theorem 3bitrrd 308

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 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	1, 4	bitr3d 283	1 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rnmpt0f  6230  sbcoteq1a  8032  fnwelem  8111  mpocurryd  8249  compssiso  10331  divfl0  13834  cjreb  15150  cnpart  15267  bitsuz  16508  acsfn  17691  eqg0el  19224  ghmeqker  19283  odmulg  19596  psrbaglefi  21975  cnrest2  23343  hausdiag  23702  prdsbl  24548  mcubic  26909  2lgslem1a2  27451  fmptco1f1o  32832  qsidomlem2  33637  areacirclem4  38207  lmclim2  38254  cmtbr2N  39874  expdiophlem1  43595  cantnfresb  43898  rrx2linest  49361