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  6143  fnwelem  7956  mpocurryd  8069  compssiso  10114  divfl0  13525  cjreb  14815  cnpart  14932  bitsuz  16162  acsfn  17349  ghmeqker  18842  odmulg  19144  psrbaglefi  21116  psrbaglefiOLD  21117  cnrest2  22418  hausdiag  22777  prdsbl  23628  mcubic  25978  2lgslem1a2  26519  fmptco1f1o  30947  eqg0el  31536  qsidomlem2  31608  sbcoteq1a  33666  areacirclem4  35847  lmclim2  35895  cmtbr2N  37246  expdiophlem1  40823  rrx2linest  46040