ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antll Structured version   Unicode version

Theorem ad2antll 460
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1
Assertion
Ref Expression
ad2antll

Proof of Theorem ad2antll
StepHypRef Expression
1 ad2ant.1 . . 3
21adantl 262 . 2
32adantl 262 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  simprr  484  simprrl  491  simprrr  492  dn1dc  866  prneimg  3536  f1oprg  5111  subhalfnqq  6397  nqnq0pi  6421  genprndl  6504  genprndu  6505  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  mullocpr  6552  ltaprlem  6591  aptiprleml  6611  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemladdfu  6648  mulcmpblnrlemg  6668  recexgt0sr  6701  pitonn  6744  rimul  7369  receuap  7432  peano5uzti  8122  iooshf  8591  iseqfveq2  8905  expcl2lemap  8921  mulexpzap  8949  expnlbnd2  9027
  Copyright terms: Public domain W3C validator