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

Theorem 3bitr2rd 296
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 270 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitr2d 268 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  fnsuppres  7187  addsubeq4  10148  muleqadd  10523  mulle0b  10746  adddivflid  12439  om2uzlti  12569  summodnegmod  14799  qnumdenbi  15239  dprdf11  18194  lvecvscan2  18882  mdetunilem9  20193  elfilss  21438  itg2seq  23260  itg2cnlem2  23280  chpchtsum  24689  bposlem7  24760  lgsdilem  24794  lgsne0  24805  colhp  25408  axcontlem7  25596  pjnorm2  27764  cdj3lem1  28471  zrhchr  29142  dochfln0  35578  mapdindp  35772
  Copyright terms: Public domain W3C validator