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  6263  sbcoteq1a  8097  fnwelem  8180  mpocurryd  8324  compssiso  10491  divfl0  14004  cjreb  15333  cnpart  15450  bitsuz  16688  acsfn  17883  eqg0el  19448  ghmeqker  19507  odmulg  19821  qsidomlem2  21688  psrbaglefi  22289  cnrest2  23659  hausdiag  24019  prdsbl  24865  mcubic  27232  2lgslem1a2  27774  fmptco1f1o  33325  areacirclem4  38897  lmclim2  38958  cmtbr2N  40576  expdiophlem1  44294  cantnfresb  44587  rrx2linest  50185