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  6086  fnwelem  7876  mpocurryd  7989  compssiso  9953  divfl0  13364  cjreb  14651  cnpart  14768  bitsuz  15996  acsfn  17116  ghmeqker  18603  odmulg  18901  psrbaglefi  20845  psrbaglefiOLD  20846  cnrest2  22137  hausdiag  22496  prdsbl  23343  mcubic  25684  2lgslem1a2  26225  fmptco1f1o  30641  eqg0el  31225  qsidomlem2  31297  sbcoteq1a  33357  areacirclem4  35554  lmclim2  35602  cmtbr2N  36953  expdiophlem1  40487  rrx2linest  45704