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 ⊢ (𝜑 → (𝜏 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rnmpt0f  6244  sbcoteq1a  8044  fnwelem  8123  mpocurryd  8261  compssiso  10353  divfl0  13853  cjreb  15170  cnpart  15287  bitsuz  16527  acsfn  17710  eqg0el  19249  ghmeqker  19308  odmulg  19621  qsidomlem2  21481  psrbaglefi  22076  cnrest2  23443  hausdiag  23802  prdsbl  24648  mcubic  27012  2lgslem1a2  27554  fmptco1f1o  32978  areacirclem4  38362  lmclim2  38409  cmtbr2N  40027  expdiophlem1  43748  cantnfresb  44051  rrx2linest  49522