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:  fnwelem  7819  mpocurryd  7929  compssiso  9790  divfl0  13188  cjreb  14476  cnpart  14593  bitsuz  15817  acsfn  16924  ghmeqker  18379  odmulg  18677  psrbaglefi  20146  cnrest2  21888  hausdiag  22247  prdsbl  23095  mcubic  25419  2lgslem1a2  25960  fmptco1f1o  30372  eqg0el  30921  qsidomlem2  30961  areacirclem4  34979  lmclim2  35027  cmtbr2N  36383  expdiophlem1  39611  rnmpt0  41476  rrx2linest  44723