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 205

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 206

This theorem is referenced by:  rnmpt0f  6161  fnwelem  8003  mpocurryd  8116  compssiso  10180  divfl0  13594  cjreb  14883  cnpart  15000  bitsuz  16230  acsfn  17417  ghmeqker  18910  odmulg  19212  psrbaglefi  21184  psrbaglefiOLD  21185  cnrest2  22486  hausdiag  22845  prdsbl  23696  mcubic  26046  2lgslem1a2  26587  fmptco1f1o  31017  eqg0el  31606  qsidomlem2  31678  sbcoteq1a  33736  areacirclem4  35916  lmclim2  35964  cmtbr2N  37467  expdiophlem1  41039  rrx2linest  46332