Theorem 3bitrrd 305

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rnmpt0f  6242  sbcoteq1a  8036  fnwelem  8116  mpocurryd  8253  compssiso  10368  divfl0  13788  cjreb  15069  cnpart  15186  bitsuz  16414  acsfn  17602  ghmeqker  19118  odmulg  19423  psrbaglefi  21484  psrbaglefiOLD  21485  cnrest2  22789  hausdiag  23148  prdsbl  23999  mcubic  26349  2lgslem1a2  26890  fmptco1f1o  31852  eqg0el  32468  qsidomlem2  32567  areacirclem4  36574  lmclim2  36621  cmtbr2N  38118  expdiophlem1  41750  cantnfresb  42064  rrx2linest  47418