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

Theorem 3bitrrd 295
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 269 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 270 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  fnwelem  7443  mpt2curryd  7547  compssiso  9398  divfl0  12833  cjreb  14071  cnpart  14188  bitsuz  15404  acsfn  16527  ghmeqker  17895  odmulg  18180  psrbaglefi  19587  cnrest2  21311  hausdiag  21669  prdsbl  22516  mcubic  24795  2lgslem1a2  25336  fmptco1f1o  29774  areacirclem4  33835  lmclim2  33886  cmtbr2N  35062  expdiophlem1  38114  rnmpt0  39930
  Copyright terms: Public domain W3C validator