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

Theorem ad2antll 482
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 275 . 2  |-  ( ( th  /\  ph )  ->  ps )
32adantl 275 1  |-  ( ( ch  /\  ( th 
/\  ph ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simprr  521  simprrl  528  simprrr  529  dn1dc  944  prneimg  3701  f1oprg  5411  fvco4  5493  nnsucuniel  6391  mapen  6740  mapxpen  6742  fidceq  6763  fidifsnen  6764  php5fin  6776  findcard2d  6785  findcard2sd  6786  diffisn  6787  fidcenumlemr  6843  supmoti  6880  djuf1olem  6938  exmidfodomrlemim  7057  cc4f  7084  cc4n  7086  subhalfnqq  7229  nqnq0pi  7253  genprndl  7336  genprndu  7337  addlocpr  7351  nqprl  7366  nqpru  7367  addnqprlemrl  7372  addnqprlemru  7373  mullocpr  7386  mulnqprlemrl  7388  mulnqprlemru  7389  ltaprlem  7433  aptiprleml  7454  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  caucvgprlemladdfu  7492  caucvgprprlemloc  7518  suplocexprlemrl  7532  suplocexprlemru  7534  mulcmpblnrlemg  7555  recexgt0sr  7588  pitonn  7663  rereceu  7704  rimul  8354  receuap  8437  peano5uzti  9166  iooshf  9742  seq3fveq2  10249  seq3id2  10289  seqfeq3  10292  expcl2lemap  10312  mulexpzap  10340  expnlbnd2  10424  hashfacen  10586  absexpzap  10859  fsumf1o  11166  fisum0diag2  11223  fsummulc2  11224  moddvds  11509  dvdsflip  11556  dfgcd3  11705  dfgcd2  11709  lcmgcdlem  11765  cncongr1  11791  hashgcdlem  11910  setscom  12009  tgcl  12243  epttop  12269  cnpnei  12398  txcn  12454  txdis1cn  12457  imasnopn  12478  hmeoimaf1o  12493  txhmeo  12498  metss2lem  12676  bdxmet  12680  bdmopn  12683  metrest  12685  xmetxp  12686  metcnp  12691
  Copyright terms: Public domain W3C validator