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

Theorem ad2antll 468
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antll  |-  ( ( ch  /\  ( th 
/\  ph ) )  ->  ps )

Proof of Theorem ad2antll
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantl 266 . 2  |-  ( ( th  /\  ph )  ->  ps )
32adantl 266 1  |-  ( ( ch  /\  ( th 
/\  ph ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  simprr  492  simprrl  499  simprrr  500  dn1dc  878  prneimg  3572  f1oprg  5195  fidceq  6360  fidifsnen  6361  php5fin  6369  findcard2d  6378  findcard2sd  6379  diffisn  6380  supmoti  6398  subhalfnqq  6569  nqnq0pi  6593  genprndl  6676  genprndu  6677  addlocpr  6691  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  mullocpr  6726  mulnqprlemrl  6728  mulnqprlemru  6729  ltaprlem  6773  aptiprleml  6794  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  caucvgprlemladdfu  6832  caucvgprprlemloc  6858  mulcmpblnrlemg  6882  recexgt0sr  6915  pitonn  6981  rereceu  7020  rimul  7649  receuap  7723  peano5uzti  8404  iooshf  8921  iseqfveq2  9391  expcl2lemap  9431  mulexpzap  9459  expnlbnd2  9541  absexpzap  9906  moddvds  10116  dvdsflip  10162
  Copyright terms: Public domain W3C validator