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  2830  frecsuclem  6572  indpi  7562  cauappcvgprlemladdru  7876  prsrlt  8007  lesub2  8637  ltsub2  8639  rec11ap  8890  avglt1  9383  rpnegap  9921  modqmuladdnn0  10631  expap0  10832  swrdspsleq  11249  2shfti  11393  mulreap  11426  minmax  11792  lemininf  11796  xrminmax  11827  xrlemininf  11833  modremain  12492  nnwosdc  12612  nn0seqcvgd  12615  divgcdcoprm0  12675  ismgmid  13462  grpsubeq0  13671  grpsubadd  13673  eqg0el  13818  isunitd  14123  lsslss  14398  isridlrng  14499  zndvds  14666  znleval  14670  isxmet2d  15075  xblss2  15132  neibl  15218  ellimc3apf  15387  logbgt0b  15693  lgsne0  15770  lgsabs1  15771  lgsquadlem1  15809  m1lgs  15817  eupth2lem2dc  16313  eupth2lem3lem4fi  16327  iswomninnlem  16674
  Copyright terms: Public domain W3C validator