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

Theorem ad2antlr 473
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antlr  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 270 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 460 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
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:  ad3antlr  477  simplr  497  simplrl  502  simplrr  503  ordtri2or2exmidlem  4317  en2lp  4345  xpid11m  4628  foun  5237  f1oprg  5260  fcof1o  5531  foeqcnvco  5532  f1eqcocnv  5533  caovord3  5777  f1o2ndf1  5952  smores2  6015  frecrdg  6129  nnaordex  6240  xpdom2  6501  xpen  6515  mapen  6516  xpmapenlem  6519  nndomo  6534  phpm  6535  fidifsnen  6540  isinfinf  6567  finexdc  6572  fientri3  6579  xpfi  6593  f1dmvrnfibi  6606  sbthlemi8  6620  djudom  6734  enomnilem  6741  finomni  6743  exmidfodomrlemrALT  6776  dfplpq2  6860  recclnq  6898  subhalfnqq  6920  distrnq0  6965  prarloclem3step  7002  genpml  7023  genpmu  7024  addnqprl  7035  addnqpru  7036  appdivnq  7069  mulnqprl  7074  mulnqpru  7075  mullocpr  7077  ltexprlemfl  7115  ltexprlemfu  7117  ltmprr  7148  archpr  7149  cauappcvgprlemm  7151  caucvgprlemladdrl  7184  caucvgprprlemopl  7203  caucvgprprlemopu  7205  recexgt0sr  7266  mulgt0sr  7270  elrealeu  7314  axcaucvglemcau  7380  axcaucvglemres  7381  cnegex  7607  apirr  8026  mulge0  8040  lemul12a  8261  lediv2a  8294  creur  8357  nndiv  8400  zaddcllemneg  8725  peano5uzti  8790  supinfneg  9018  infsupneg  9019  divfnzn  9041  xrltso  9201  elioc2  9289  elico2  9290  elicc2  9291  exfzdc  9582  exbtwnzlemex  9592  rebtwn2z  9597  modqid  9687  modqcyc  9697  mulqaddmodid  9702  modqadd2mod  9712  addmodlteq  9736  frecuzrdgg  9754  iseqvalt  9804  iseqclt  9815  iseqoveq  9816  iseqf1olemqcl  9839  iseqf1olemnab  9841  iseqf1olemp  9855  iseqf1o  9857  fser0const  9871  ser3ge0  9872  facndiv  10065  faclbnd  10067  ibcval5  10089  hashen  10110  fihashdom  10129  hashunlem  10130  hashfacen  10159  zfz1isolemiso  10162  iseqcoll  10165  caucvgre  10331  resqrexlemlo  10363  cau3lem  10464  qdenre  10552  rexico  10571  fimaxre2  10574  2clim  10605  cn1lem  10618  climsqz  10639  climsqz2  10640  climcau  10650  isumrblem  10679  isummolem2a  10684  fisum  10689  fsumcl2lem  10699  fsumadd  10707  sumsnf  10710  zdvdsdc  10742  dvdseq  10774  dvdsext  10781  odd2np1  10798  sqoddm1div8z  10811  nno  10831  zsupcllemstep  10866  infssuzex  10870  dfgcd3  10924  dvdslcm  10976  lcmneg  10981  lcmgcdlem  10984  ncoprmgcdne1b  10996  qredeq  11003  qredeu  11004  divgcdcoprm0  11008  exprmfct  11044  prmdvdsfz  11045  rpexp1i  11058  sqrt2irr  11066  nonsq  11110  nnsf  11383  peano4nninf  11384  nninfalllemn  11386  nninfalllem1  11387  nninfsellemqall  11395  nninfsellemeqinf  11396  exmidsbthrlem  11400
  Copyright terms: Public domain W3C validator