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  8335  mulge0  8349  lemul12a  8588  lediv2a  8621  creur  8685  nndiv  8729  zaddcllemneg  9061  peano5uzti  9127  supinfneg  9358  infsupneg  9359  divfnzn  9381  xrltso  9550  xpncan  9622  xltadd1  9627  xleaddadd  9638  elioc2  9687  elico2  9688  elicc2  9689  exfzdc  9985  exbtwnzlemex  9995  rebtwn2z  10000  modqid  10090  modqcyc  10100  mulqaddmodid  10105  modqadd2mod  10115  addmodlteq  10139  frecuzrdgg  10157  seq3val  10199  seqvalcd  10200  seq3clss  10208  iseqf1olemqcl  10227  iseqf1olemnab  10229  seq3f1olemp  10243  seq3f1o  10245  fser0const  10257  ser3ge0  10258  exp3vallem  10262  facndiv  10453  faclbnd  10455  bcval5  10477  hashen  10498  fihashdom  10517  hashunlem  10518  hashfacen  10547  zfz1isolemiso  10550  seq3coll  10553  caucvgre  10721  resqrexlemlo  10753  cau3lem  10854  qdenre  10942  rexico  10961  fimaxre2  10966  xrmaxiflemcl  10982  xrmaxifle  10983  xrmaxiflemcom  10986  2clim  11038  cn1lem  11051  climsqz  11072  climsqz2  11073  climcau  11084  sumrbdclem  11113  summodclem2a  11118  fsum3  11124  fsumcl2lem  11135  fsumadd  11143  sumsnf  11146  fsum2dlemstep  11171  fisum0diag2  11184  fsummulc2  11185  mertenslemub  11271  mertenslemi1  11272  mertensabs  11274  efaddlem  11307  tanaddaplem  11372  zdvdsdc  11441  dvdseq  11473  dvdsext  11480  odd2np1  11497  sqoddm1div8z  11510  nno  11530  zsupcllemstep  11565  infssuzex  11569  dfgcd3  11625  dvdslcm  11677  lcmneg  11682  lcmgcdlem  11685  ncoprmgcdne1b  11697  qredeq  11704  qredeu  11705  divgcdcoprm0  11709  exprmfct  11745  prmdvdsfz  11746  rpexp1i  11759  sqrt2irr  11767  nonsq  11812  ctinfom  11868  enctlem  11872  setsfun  11921  setsfun0  11922  setscom  11926  tgdom  12168  ssrest  12278  cnfval  12290  cnpfval  12291  cnpval  12294  iscnp3  12299  ssidcn  12306  cnpnei  12315  cnntr  12321  cncnp  12326  cnptopresti  12334  tx1cn  12365  upxp  12368  imasnopn  12395  bdmet  12598  metcnp  12608  ivthinclemlr  12711  ivthinclemur  12713  ivthinc  12717  dvrecap  12773  pilem3  12791  nnsf  13126  peano4nninf  13127  nninfalllemn  13129  nninfalllem1  13130  nninfsellemqall  13138  nninfsellemeqinf  13139  nninffeq  13143  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator