ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2antll GIF 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  867  prneimg  3545  f1oprg  5168  fidceq  6330  fidifsnen  6331  php5fin  6339  findcard2d  6348  findcard2sd  6349  diffisn  6350  subhalfnqq  6512  nqnq0pi  6536  genprndl  6619  genprndu  6620  addlocpr  6634  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  ltaprlem  6716  aptiprleml  6737  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemladdfu  6775  caucvgprprlemloc  6801  mulcmpblnrlemg  6825  recexgt0sr  6858  pitonn  6924  rereceu  6963  rimul  7576  receuap  7650  peano5uzti  8346  iooshf  8821  iseqfveq2  9228  expcl2lemap  9267  mulexpzap  9295  expnlbnd2  9374  absexpzap  9676
  Copyright terms: Public domain W3C validator