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

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

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3
21adantr 261 . 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:  simprl  483  simprll  489  simprlr  490  elxp5  4752  f1oprg  5111  cnvf1olem  5787  nnaordi  6017  swoer  6070  0er  6076  enq0sym  6415  nqnq0pi  6421  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  archpr  6615  cauappcvgprlemloc  6624  cauappcvgprlemladdfl  6627  caucvgprlemdisj  6645  caucvgprlemloc  6646  mulcmpblnrlemg  6668  axarch  6773  cnegexlem2  6984  mulge0  7403  divdivap1  7481  divdivap2  7482  conjmulap  7487  ltdivmul  7623  nn0ge0div  8103  peano2uz2  8121  peano5uzti  8122  eluzp1m1  8272  iooshf  8591  divelunit  8640  eluzgtdifelfzo  8823  iseqval  8900  iseqfveq2  8905  expineg2  8918  mulexpzap  8949  leexp2r  8962  expnlbnd2  9027
  Copyright terms: Public domain W3C validator