ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr2d GIF version

Theorem 3bitr2d 216
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1 (𝜑 → (𝜓𝜒))
3bitr2d.2 (𝜑 → (𝜃𝜒))
3bitr2d.3 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3bitr2d (𝜑 → (𝜓𝜏))

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3 (𝜑 → (𝜓𝜒))
2 3bitr2d.2 . . 3 (𝜑 → (𝜃𝜒))
31, 2bitr4d 191 . 2 (𝜑 → (𝜓𝜃))
4 3bitr2d.3 . 2 (𝜑 → (𝜃𝜏))
53, 4bitrd 188 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ceqsralt  2779  frecsuclem  6432  indpi  7372  cauappcvgprlemladdru  7686  prsrlt  7817  lesub2  8445  ltsub2  8447  rec11ap  8698  avglt1  9188  rpnegap  9718  modqmuladdnn0  10401  expap0  10584  2shfti  10875  mulreap  10908  minmax  11273  lemininf  11277  xrminmax  11308  xrlemininf  11314  modremain  11969  nnwosdc  12075  nn0seqcvgd  12076  divgcdcoprm0  12136  ismgmid  12856  grpsubeq0  13045  grpsubadd  13047  eqg0el  13185  isunitd  13473  lsslss  13714  isridlrng  13815  isxmet2d  14325  xblss2  14382  neibl  14468  ellimc3apf  14606  logbgt0b  14861  lgsne0  14917  lgsabs1  14918  m1lgs  14930  iswomninnlem  15276
  Copyright terms: Public domain W3C validator