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

Theorem 3bitr2rd 297
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1 (𝜑 → (𝜓𝜒))
3bitr2d.2 (𝜑 → (𝜃𝜒))
3bitr2d.3 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3bitr2rd (𝜑 → (𝜏𝜓))

Proof of Theorem 3bitr2rd
StepHypRef Expression
1 3bitr2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitr2d.2 . . 3 (𝜑 → (𝜃𝜒))
31, 2bitr4d 271 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitr2d 269 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:  fnsuppres  7478  addsubeq4  10502  muleqadd  10877  mulle0b  11100  adddivflid  12827  om2uzlti  12957  summodnegmod  15221  qnumdenbi  15659  dprdf11  18630  lvecvscan2  19325  mdetunilem9  20644  elfilss  21900  itg2seq  23729  itg2cnlem2  23749  chpchtsum  25165  bposlem7  25236  lgsdilem  25270  lgsne0  25281  colhp  25883  axcontlem7  26071  pjnorm2  28926  cdj3lem1  29633  zrhchr  30360  dochfln0  37285  mapdindp  37479
  Copyright terms: Public domain W3C validator