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  6246  sbcoteq1a  8054  fnwelem  8133  mpocurryd  8271  compssiso  10373  divfl0  13875  cjreb  15198  cnpart  15315  bitsuz  16554  acsfn  17737  eqg0el  19298  ghmeqker  19357  odmulg  19670  qsidomlem2  21531  psrbaglefi  22126  cnrest2  23493  hausdiag  23853  prdsbl  24699  mcubic  27063  2lgslem1a2  27605  fmptco1f1o  33049  areacirclem4  38419  lmclim2  38467  cmtbr2N  40085  expdiophlem1  43806  cantnfresb  44109  rrx2linest  49579