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  6249  sbcoteq1a  8056  fnwelem  8136  mpocurryd  8275  compssiso  10404  divfl0  13830  cjreb  15114  cnpart  15231  bitsuz  16460  acsfn  17658  eqg0el  19163  ghmeqker  19223  odmulg  19540  psrbaglefi  21899  psrbaglefiOLD  21900  cnrest2  23251  hausdiag  23610  prdsbl  24461  mcubic  26844  2lgslem1a2  27388  fmptco1f1o  32519  qsidomlem2  33286  areacirclem4  37335  lmclim2  37382  cmtbr2N  38875  expdiophlem1  42589  cantnfresb  42900  rrx2linest  48006