Theorem 3bitrrd 307

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  rnmpt0f  6194  sbcoteq1a  7993  fnwelem  8071  mpocurryd  8209  compssiso  10287  divfl0  13774  cjreb  15076  cnpart  15193  bitsuz  16434  acsfn  17616  eqg0el  19149  ghmeqker  19209  odmulg  19522  psrbaglefi  21901  cnrest2  23269  hausdiag  23628  prdsbl  24474  mcubic  26829  2lgslem1a2  27371  fmptco1f1o  32725  qsidomlem2  33536  areacirclem4  38078  lmclim2  38125  cmtbr2N  39745  expdiophlem1  43466  cantnfresb  43769  rrx2linest  49233