Theorem 3bitrrd 306

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 280	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	1, 4	bitr3d 281	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  6243  sbcoteq1a  8037  fnwelem  8117  mpocurryd  8254  compssiso  10369  divfl0  13789  cjreb  15070  cnpart  15187  bitsuz  16415  acsfn  17603  ghmeqker  19119  odmulg  19424  psrbaglefi  21485  psrbaglefiOLD  21486  cnrest2  22790  hausdiag  23149  prdsbl  24000  mcubic  26352  2lgslem1a2  26893  fmptco1f1o  31888  eqg0el  32504  qsidomlem2  32603  areacirclem4  36627  lmclim2  36674  cmtbr2N  38171  expdiophlem1  41808  cantnfresb  42122  rrx2linest  47476