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  6243  sbcoteq1a  8060  fnwelem  8141  mpocurryd  8279  compssiso  10445  divfl0  13957  cjreb  15283  cnpart  15400  bitsuz  16637  acsfn  17826  eqg0el  19391  ghmeqker  19450  odmulg  19763  qsidomlem2  21630  psrbaglefi  22227  cnrest2  23597  hausdiag  23957  prdsbl  24803  mcubic  27168  2lgslem1a2  27710  fmptco1f1o  33220  areacirclem4  38609  lmclim2  38672  cmtbr2N  40290  expdiophlem1  44007  cantnfresb  44310  rrx2linest  49823