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

Theorem ad2antll 475
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 271 . 2 ((𝜃𝜑) → 𝜓)
32adantl 271 1 ((𝜒 ∧ (𝜃𝜑)) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simprr  499  simprrl  506  simprrr  507  dn1dc  902  prneimg  3587  f1oprg  5221  nnsucuniel  6161  fidceq  6427  fidifsnen  6428  php5fin  6440  findcard2d  6449  findcard2sd  6450  diffisn  6451  supmoti  6502  djulf1o  6557  djurf1o  6558  subhalfnqq  6743  nqnq0pi  6767  genprndl  6850  genprndu  6851  addlocpr  6865  nqprl  6880  nqpru  6881  addnqprlemrl  6886  addnqprlemru  6887  mullocpr  6900  mulnqprlemrl  6902  mulnqprlemru  6903  ltaprlem  6947  aptiprleml  6968  cauappcvgprlemladdfu  6983  cauappcvgprlemladdfl  6984  caucvgprlemladdfu  7006  caucvgprprlemloc  7032  mulcmpblnrlemg  7056  recexgt0sr  7089  pitonn  7155  rereceu  7194  rimul  7829  receuap  7903  peano5uzti  8613  iooshf  9128  iseqfveq2  9621  iseqid2  9641  expcl2lemap  9662  mulexpzap  9690  expnlbnd2  9772  absexpzap  10192  moddvds  10437  dvdsflip  10484  dfgcd3  10631  dfgcd2  10635  lcmgcdlem  10691  cncongr1  10717  hashgcdlem  10835
  Copyright terms: Public domain W3C validator