MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrrd Structured version   Visualization version   GIF version

Theorem 3bitrrd 293
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
StepHypRef Expression
1 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
2 3bitrd.1 . . 3 (𝜑 → (𝜓𝜒))
3 3bitrd.2 . . 3 (𝜑 → (𝜒𝜃))
42, 3bitr2d 267 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 268 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  fnwelem  7156  mpt2curryd  7259  compssiso  9056  divfl0  12444  cjreb  13659  cnpart  13776  bitsuz  14982  acsfn  16091  ghmeqker  17458  odmulg  17744  psrbaglefi  19141  cnrest2  20847  hausdiag  21205  prdsbl  22053  mcubic  24318  2lgslem1a2  24859  cusgra3v  25786  areacirclem4  32456  lmclim2  32507  cmtbr2N  33341  expdiophlem1  36389  rnmpt0  38190
  Copyright terms: Public domain W3C validator