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

Theorem 3bitr2rd 310
 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 284 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitr2d 282 1 (𝜑 → (𝜏𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208 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 209 This theorem is referenced by:  fnsuppres  7849  addsubeq4  10893  muleqadd  11276  mulle0b  11503  adddivflid  13180  om2uzlti  13310  summodnegmod  15632  qnumdenbi  16076  dprdf11  19137  lvecvscan2  19876  mdetunilem9  21221  elfilss  22476  mbfmulc2lem  24240  itg2seq  24335  itg2cnlem2  24355  chpchtsum  25787  bposlem7  25858  lgsdilem  25892  lgsne0  25903  colhp  26548  axcontlem7  26748  pjnorm2  29496  cdj3lem1  30203  zrhchr  31210  dochfln0  38605  mapdindp  38799
 Copyright terms: Public domain W3C validator