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 206

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 207

This theorem is referenced by:  rnmpt0f  6190  sbcoteq1a  7983  fnwelem  8061  mpocurryd  8199  compssiso  10265  divfl0  13728  cjreb  15030  cnpart  15147  bitsuz  16385  acsfn  17565  eqg0el  19095  ghmeqker  19155  odmulg  19468  psrbaglefi  21863  cnrest2  23201  hausdiag  23560  prdsbl  24406  mcubic  26784  2lgslem1a2  27328  fmptco1f1o  32615  qsidomlem2  33418  areacirclem4  37759  lmclim2  37806  cmtbr2N  39300  expdiophlem1  43062  cantnfresb  43365  rrx2linest  48782