Theorem 3bitrrd 305

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 279	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	1, 4	bitr3d 280	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  6181  fnwelem  8039  mpocurryd  8155  compssiso  10231  divfl0  13645  cjreb  14933  cnpart  15050  bitsuz  16280  acsfn  17465  ghmeqker  18957  odmulg  19259  psrbaglefi  21241  psrbaglefiOLD  21242  cnrest2  22543  hausdiag  22902  prdsbl  23753  mcubic  26103  2lgslem1a2  26644  fmptco1f1o  31255  eqg0el  31853  qsidomlem2  31926  sbcoteq1a  33977  areacirclem4  35973  lmclim2  36021  cmtbr2N  37520  expdiophlem1  41106  rrx2linest  46439