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  6510  nqnq0pi  6534  genprndl  6617  genprndu  6618  addlocpr  6632  nqprl  6647  nqpru  6648  addnqprlemrl  6653  addnqprlemru  6654  mullocpr  6667  mulnqprlemrl  6669  mulnqprlemru  6670  ltaprlem  6714  aptiprleml  6735  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  caucvgprlemladdfu  6773  caucvgprprlemloc  6799  mulcmpblnrlemg  6823  recexgt0sr  6856  pitonn  6922  rereceu  6961  rimul  7574  receuap  7648  peano5uzti  8344  iooshf  8819  iseqfveq2  9226  expcl2lemap  9265  mulexpzap  9293  expnlbnd2  9372  absexpzap  9674
  Copyright terms: Public domain W3C validator