Theorem 3bitrrd 309

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  rnmpt0f  6239  sbcoteq1a  8048  fnwelem  8129  mpocurryd  8267  compssiso  10376  divfl0  13885  cjreb  15210  cnpart  15327  bitsuz  16564  acsfn  17747  eqg0el  19311  ghmeqker  19370  odmulg  19683  qsidomlem2  21544  psrbaglefi  22141  cnrest2  23511  hausdiag  23871  prdsbl  24717  mcubic  27084  2lgslem1a2  27626  fmptco1f1o  33106  areacirclem4  38460  lmclim2  38508  cmtbr2N  40126  expdiophlem1  43862  cantnfresb  44165  rrx2linest  49672