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

Theorem 3bitr2rd 308
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 282 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitr2d 280 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  fnsuppres  8216  addsubeq4  11523  muleqadd  11907  mulle0b  12139  adddivflid  13858  om2uzlti  13991  summodnegmod  16324  qnumdenbi  16781  dprdf11  20043  lvecvscan2  21114  mdetunilem9  22626  elfilss  23884  mbfmulc2lem  25682  itg2seq  25777  itg2cnlem2  25797  chpchtsum  27263  bposlem7  27334  lgsdilem  27368  lgsne0  27379  colhp  28778  axcontlem7  28985  pjnorm2  31746  cdj3lem1  32453  zringfrac  33582  ply1dg1rt  33604  zrhchr  33975  bj-gabima  36941  dochfln0  41479  mapdindp  41673  stgredgiun  47925
  Copyright terms: Public domain W3C validator