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

Theorem ad2antlr 480
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 274 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 467 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  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:  ad3antlr  484  simplr  504  simplrl  509  simplrr  510  ordtri2or2exmidlem  4411  en2lp  4439  foun  5354  f1oprg  5379  fcof1o  5658  foeqcnvco  5659  f1eqcocnv  5660  caovord3  5912  f1o2ndf1  6093  smores2  6159  frecrdg  6273  nnaordex  6391  xpdom2  6693  xpen  6707  mapen  6708  xpmapenlem  6711  nndomo  6726  phpm  6727  fidifsnen  6732  isinfinf  6759  finexdc  6764  fientri3  6771  fiintim  6785  xpfi  6786  f1dmvrnfibi  6800  sbthlemi8  6820  djudom  6946  omp1eomlem  6947  difinfsn  6953  ctmlemr  6961  ctssdccl  6964  enomnilem  6978  finomni  6980  ismkvnex  6997  exmidfodomrlemrALT  7027  dfplpq2  7130  recclnq  7168  subhalfnqq  7190  distrnq0  7235  prarloclem3step  7272  genpml  7293  genpmu  7294  addnqprl  7305  addnqpru  7306  appdivnq  7339  mulnqprl  7344  mulnqpru  7345  mullocpr  7347  ltexprlemfl  7385  ltexprlemfu  7387  ltmprr  7418  archpr  7419  cauappcvgprlemm  7421  caucvgprlemladdrl  7454  caucvgprprlemopl  7473  caucvgprprlemopu  7475  recexgt0sr  7549  mulgt0sr  7554  elrealeu  7605  axcaucvglemcau  7674  axcaucvglemres  7675  cnegex  7908  apirr  8334  mulge0  8348  lemul12a  8584  lediv2a  8617  creur  8681  nndiv  8725  zaddcllemneg  9051  peano5uzti  9117  supinfneg  9346  infsupneg  9347  divfnzn  9369  xrltso  9537  xpncan  9609  xltadd1  9614  xleaddadd  9625  elioc2  9674  elico2  9675  elicc2  9676  exfzdc  9972  exbtwnzlemex  9982  rebtwn2z  9987  modqid  10077  modqcyc  10087  mulqaddmodid  10092  modqadd2mod  10102  addmodlteq  10126  frecuzrdgg  10144  seq3val  10186  seqvalcd  10187  seq3clss  10195  iseqf1olemqcl  10214  iseqf1olemnab  10216  seq3f1olemp  10230  seq3f1o  10232  fser0const  10244  ser3ge0  10245  exp3vallem  10249  facndiv  10440  faclbnd  10442  bcval5  10464  hashen  10485  fihashdom  10504  hashunlem  10505  hashfacen  10534  zfz1isolemiso  10537  seq3coll  10540  caucvgre  10708  resqrexlemlo  10740  cau3lem  10841  qdenre  10929  rexico  10948  fimaxre2  10953  xrmaxiflemcl  10969  xrmaxifle  10970  xrmaxiflemcom  10973  2clim  11025  cn1lem  11038  climsqz  11059  climsqz2  11060  climcau  11071  sumrbdclem  11100  summodclem2a  11105  fsum3  11111  fsumcl2lem  11122  fsumadd  11130  sumsnf  11133  fsum2dlemstep  11158  fisum0diag2  11171  fsummulc2  11172  mertenslemub  11258  mertenslemi1  11259  mertensabs  11261  efaddlem  11294  tanaddaplem  11359  zdvdsdc  11426  dvdseq  11458  dvdsext  11465  odd2np1  11482  sqoddm1div8z  11495  nno  11515  zsupcllemstep  11550  infssuzex  11554  dfgcd3  11610  dvdslcm  11662  lcmneg  11667  lcmgcdlem  11670  ncoprmgcdne1b  11682  qredeq  11689  qredeu  11690  divgcdcoprm0  11694  exprmfct  11730  prmdvdsfz  11731  rpexp1i  11744  sqrt2irr  11752  nonsq  11796  ctinfom  11852  enctlem  11856  setsfun  11905  setsfun0  11906  setscom  11910  tgdom  12152  ssrest  12262  cnfval  12274  cnpfval  12275  cnpval  12278  iscnp3  12283  ssidcn  12290  cnpnei  12299  cnntr  12305  cncnp  12310  cnptopresti  12318  tx1cn  12349  upxp  12352  imasnopn  12379  bdmet  12582  metcnp  12592  ivthinclemlr  12695  ivthinclemur  12697  ivthinc  12701  dvrecap  12757  pilem3  12775  nnsf  13095  peano4nninf  13096  nninfalllemn  13098  nninfalllem1  13099  nninfsellemqall  13107  nninfsellemeqinf  13108  nninffeq  13112  exmidsbthrlem  13113
  Copyright terms: Public domain W3C validator