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  7209  addsubeq4  10175  muleqadd  10550  mulle0b  10773  adddivflid  12481  om2uzlti  12611  summodnegmod  14850  qnumdenbi  15290  dprdf11  18245  lvecvscan2  18933  mdetunilem9  20245  elfilss  21490  itg2seq  23315  itg2cnlem2  23335  chpchtsum  24744  bposlem7  24815  lgsdilem  24849  lgsne0  24860  colhp  25462  axcontlem7  25650  pjnorm2  27970  cdj3lem1  28677  zrhchr  29348  dochfln0  35784  mapdindp  35978
 Copyright terms: Public domain W3C validator