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  7491  addsubeq4  10488  muleqadd  10863  mulle0b  11086  adddivflid  12813  om2uzlti  12943  summodnegmod  15214  qnumdenbi  15654  dprdf11  18622  lvecvscan2  19314  mdetunilem9  20628  elfilss  21881  itg2seq  23708  itg2cnlem2  23728  chpchtsum  25143  bposlem7  25214  lgsdilem  25248  lgsne0  25259  colhp  25861  axcontlem7  26049  pjnorm2  28895  cdj3lem1  29602  zrhchr  30329  dochfln0  37268  mapdindp  37462
  Copyright terms: Public domain W3C validator