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

Theorem 3bitrrd 307
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 281 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 282 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  fnwelem  7814  mpocurryd  7924  compssiso  9784  divfl0  13182  cjreb  14470  cnpart  14587  bitsuz  15811  acsfn  16918  ghmeqker  18323  odmulg  18612  psrbaglefi  20080  cnrest2  21822  hausdiag  22181  prdsbl  23028  mcubic  25352  2lgslem1a2  25893  fmptco1f1o  30306  eqg0el  30853  qsidomlem2  30883  areacirclem4  34866  lmclim2  34914  cmtbr2N  36269  expdiophlem1  39496  rnmpt0  41359  rrx2linest  44657
  Copyright terms: Public domain W3C validator