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

Theorem ad2antrr 488
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
ad2antrr  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ps )

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 276 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantlr 477 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  ad3antrrr  492  ad5ant13  519  ad5ant23  522  simpll  527  simplll  533  simpllr  534  vtoclgft  2787  reupick  3419  euotd  4250  frirrg  4346  ralxfrd  4458  nnsucpred  4612  foun  5475  f1oprg  5500  dffo4  5659  foeqcnvco  5784  fliftfun  5790  isotr  5810  riotass2  5850  ovmpodxf  5993  mpoxopoveq  6234  tfrlem1  6302  tfrlemibacc  6320  tfrlemibfn  6322  tfrlemi14d  6327  tfrexlem  6328  tfr1onlembacc  6336  tfr1onlembfn  6338  tfr1onlemres  6343  tfrcllembacc  6349  tfrcllembfn  6351  tfrcllemres  6356  frecabcl  6393  nnmordi  6510  eroprf  6621  f1imaen2g  6786  xpen  6838  mapen  6839  mapdom1g  6840  mapxpen  6841  xpmapenlem  6842  phplem4dom  6855  nndomo  6857  phpm  6858  fidifsnen  6863  dif1enen  6873  fisbth  6876  fimax2gtrilemstep  6893  fimax2gtri  6894  en2eqpr  6900  unsnfidcex  6912  unsnfidcel  6913  ssfirab  6926  fidcenumlemrks  6945  sbthlemi8  6956  fiuni  6970  ordiso2  7027  updjud  7074  difinfsnlem  7091  ctssdclemn0  7102  ctssdccl  7103  ctssdc  7105  enumctlemm  7106  enumct  7107  nnnninfeq  7119  nninfisol  7124  enomnilem  7129  fodju0  7138  enmkvlem  7152  enwomnilem  7160  nninfwlpoimlemg  7166  exmidfodomrlemim  7193  exmidontriimlem2  7214  cc3  7245  dfplpq2  7331  nqpi  7355  nqnq0pi  7415  nq0nn  7419  elinp  7451  elnp1st2nd  7453  genprndl  7498  genprndu  7499  addnqprllem  7504  addnqprulem  7505  addnqprl  7506  addnqpru  7507  addlocpr  7513  nqprloc  7522  prmuloc  7543  mulnqprl  7545  mulnqpru  7546  mullocpr  7548  distrlem1prl  7559  distrlem1pru  7560  ltsopr  7573  ltexprlemopl  7578  ltexprlemopu  7580  ltexprlemloc  7584  ltexprlemrl  7587  ltexprlemru  7589  addcanprleml  7591  addcanprlemu  7592  recexprlemloc  7608  recexprlem1ssl  7610  recexprlem1ssu  7611  aptiprleml  7616  aptiprlemu  7617  archpr  7620  cauappcvgprlemm  7622  cauappcvgprlemopl  7623  cauappcvgprlemlol  7624  cauappcvgprlemladdfu  7631  cauappcvgprlemladdfl  7632  cauappcvgprlemladdru  7633  archrecpr  7641  caucvgprlemnkj  7643  caucvgprlemm  7645  caucvgprlemopl  7646  caucvgprlemlol  7647  caucvgprlemdisj  7651  caucvgprlemloc  7652  caucvgprlemladdfu  7654  caucvgprprlemnkltj  7666  caucvgprprlemnkeqj  7667  caucvgprprlemnjltk  7668  caucvgprprlemml  7671  caucvgprprlemopl  7674  caucvgprprlemlol  7675  caucvgprprlemdisj  7679  caucvgprprlemexbt  7683  caucvgprprlemexb  7684  caucvgprprlemaddq  7685  suplocexprlemru  7696  suplocexprlemloc  7698  suplocexprlemex  7699  suplocexprlemub  7700  suplocexprlemlub  7701  mulgt0sr  7755  caucvgsrlemcau  7770  caucvgsrlemoffcau  7775  caucvgsrlemoffres  7777  suplocsrlemb  7783  suplocsrlempr  7784  suplocsrlem  7785  axcaucvglemcau  7875  axcaucvglemres  7876  axpre-suploclemres  7878  axsuploc  8007  cnegexlem1  8109  cnegex  8112  apsym  8540  apcotr  8541  apadd1  8542  mulext1  8546  mulge0  8553  apti  8556  aprcl  8580  conjmulap  8662  lemulge11  8799  creui  8893  nndiv  8936  zaddcllemneg  9268  suprzclex  9327  eluzuzle  9512  infregelbex  9574  divfnzn  9597  qapne  9615  xrltso  9770  xnn0dcle  9776  xnn0letri  9777  xrre  9794  xrre3  9796  xaddf  9818  xaddval  9819  xpncan  9845  xleadd1a  9847  xltadd1  9850  xleaddadd  9861  ixxss12  9880  elioc2  9910  elico2  9911  elicc2  9912  fzm1  10073  fzneuz  10074  eluzgtdifelfzo  10170  elfzonelfzo  10203  exfzdc  10213  qtri3or  10216  exbtwnzlemstep  10221  exbtwnzlemex  10223  exbtwnz  10224  modqid  10322  modqcyc2  10333  modqmuladd  10339  modqmuladdnn0  10341  modaddmodlo  10361  addmodlteq  10371  frecuzrdgrrn  10381  frec2uzrdg  10382  frecuzrdgsuc  10387  frecuzrdgsuctlem  10396  seq3clss  10440  iseqf1olemqcl  10459  iseqf1olemnab  10461  iseqf1olemab  10462  iseqf1olemmo  10465  iseqf1olemqf1o  10466  iseqf1olemjpcl  10468  iseqf1olemqpcl  10469  seq3f1olemqsumk  10472  seq3f1olemqsum  10473  seq3f1olemp  10475  seq3f1oleml  10476  seq3f1o  10477  seq3id3  10480  ser3ge0  10490  exp3val  10495  expap0  10523  qsqeqor  10603  modqexp  10619  nn0ltexp2  10661  facndiv  10690  faclbnd  10692  bcval5  10714  hashunlem  10755  hashun  10756  hashprg  10759  fiprsshashgt1  10768  hashfacen  10787  zfz1isolemiso  10790  zfz1isolem1  10791  seq3coll  10793  ovshftex  10799  2shfti  10811  seq3shft  10818  cjap  10886  caucvgrelemcau  10960  cvg1nlemcau  10964  cvg1nlemres  10965  recvguniq  10975  resqrexlemdecn  10992  resqrexlemcalc3  10996  resqrexlemcvg  10999  resqrexlemoverl  11001  leabs  11054  absexpzap  11060  ltabs  11067  abslt  11068  absle  11069  maxleim  11185  maxabslemval  11188  fimaxre2  11206  minmax  11209  2zinfmin  11222  xrmaxiflemcl  11224  xrmaxifle  11225  xrmaxiflemab  11226  xrmaxiflemlub  11227  xrmaxiflemcom  11228  xrmaxltsup  11237  xrmaxadd  11240  xrminmax  11244  xrbdtri  11255  2clim  11280  climshftlemg  11281  climsqz  11314  climsqz2  11315  climrecvg1n  11327  climcvg1nlem  11328  serf0  11331  sumrbdclem  11356  fsum3cvg  11357  summodclem3  11359  summodclem2a  11360  summodclem2  11361  zsumdc  11363  fsum3  11366  isumss  11370  fisumss  11371  fsum3cvg3  11375  fsumcl2lem  11377  fsumadd  11385  fsumsplit  11386  sumsnf  11388  fsum2d  11414  fisum0diag2  11426  fsummulc2  11427  modfsummod  11437  fsumabs  11444  fsumrelem  11450  fsumiun  11456  geoisumr  11497  cvgratnnlemseq  11505  cvgratz  11511  mertenslemi1  11514  mertenslem2  11515  mertensabs  11516  prodrbdclem  11550  fproddccvg  11551  prodmodclem3  11554  prodmodclem2a  11555  zproddc  11558  fprodseq  11562  fprodntrivap  11563  fprodssdc  11569  fprodmul  11570  prodsnf  11571  fprodsplitdc  11575  fprodsplit  11576  fprodunsn  11583  fprodcl2lem  11584  fprodap0  11600  fprod2d  11602  fprodrec  11608  fprodap0f  11615  efcj  11652  efaddlem  11653  tanaddaplem  11717  nndivides  11775  dvdsext  11831  divalglemeunn  11896  divalglemex  11897  divalglemeuneg  11898  zsupcllemstep  11916  infssuzex  11920  suprzubdc  11923  nninfdcex  11924  zsupssdc  11925  dvdsbnd  11927  bezoutlemnewy  11967  bezoutlemstep  11968  bezoutlemmain  11969  bezoutlemzz  11973  bezoutlemaz  11974  bezoutlembz  11975  bezoutlemeu  11978  bezoutlemle  11979  bezoutlemsup  11980  dfgcd3  11981  dfgcd2  11985  bezoutr1  12004  nnmindc  12005  dvdslcm  12039  lcmgcdlem  12047  qredeq  12066  qredeu  12067  divgcdcoprm0  12071  divgcdcoprmex  12072  cncongr1  12073  isprm2lem  12086  prmind2  12090  exprmfct  12108  prmdvdsfz  12109  isprm5lem  12111  prmexpb  12121  rpexp1i  12124  sqrt2irr  12132  sqne2sq  12147  nonsq  12177  phiprmpw  12192  eulerthlemrprm  12199  eulerthlema  12200  hashgcdeq  12209  phisum  12210  modprmn0modprm0  12226  pclemub  12257  pclemdc  12258  pcmul  12271  pcqmul  12273  pcdvdstr  12296  pcprmpw2  12302  difsqpwdvds  12307  pcmpt  12311  oddprmdvds  12322  prmpwdvds  12323  pockthg  12325  infpnlem1  12327  1arith  12335  4sqlem2  12357  ennnfonelemg  12374  ennnfoneleminc  12382  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ennnfonelemex  12385  ennnfonelemhom  12386  ennnfonelemfun  12388  ennnfonelemf1  12389  ennnfonelemrn  12390  ennnfonelemdm  12391  ennnfonelemnn0  12393  ennnfonelemim  12395  exmidunben  12397  ctinfomlemom  12398  ctinf  12401  ctiunctlemudc  12408  nninfdclemlt  12422  nninfdclemf1  12423  isstruct2r  12443  mndpropd  12720  issubmnd  12722  mndissubm  12743  mhmeql  12753  grpinvnz  12817  mhmmnd  12856  mulgfng  12863  mulgz  12886  mulgnndir  12887  mulgnn0dir  12888  mulgneg2  12892  mulgass  12895  mhmmulg  12899  issrg  12961  ringpropd  13030  ringinvnz1ne0  13039  dvdsrvald  13074  dvdsrd  13075  dvdsrtr  13082  unitgrp  13097  tgdom  13205  neipsm  13287  tgrest  13302  cnfval  13327  cnpfval  13328  cnpval  13331  iscnp4  13351  cnpnei  13352  cnptopco  13355  cncnpi  13361  cncnp  13363  cnptopresti  13371  cnptoprest2  13373  cndis  13374  lmtopcnp  13383  txbasval  13400  neitx  13401  txcnp  13404  txcnmpt  13406  txcn  13408  imasnopn  13432  psmetres2  13466  isxmet2d  13481  xblss2ps  13537  xblss2  13538  blbas  13566  neibl  13624  metss2lem  13630  metrest  13639  xmettx  13643  metcnp3  13644  metcnp  13645  metcnp2  13646  metcnpi  13648  metcnpi2  13649  mulc1cncf  13709  cncfco  13711  mulcncflem  13723  mulcncf  13724  dedekindeulemuub  13728  dedekindeulemloc  13730  dedekindeulemlu  13732  dedekindeu  13734  suplociccreex  13735  suplociccex  13736  dedekindicclemuub  13737  dedekindicclemloc  13739  dedekindicclemlu  13741  dedekindicclemicc  13743  dedekindicc  13744  ivthinclemlopn  13747  ivthinclemlr  13748  ivthinclemuopn  13749  ivthinclemur  13750  ivthinclemloc  13752  ivthinc  13754  limcimolemlt  13766  limccnp2lem  13778  limccnp2cntop  13779  limccoap  13780  dvcj  13806  dveflem  13820  efltlemlt  13828  sin0pilem1  13835  sin0pilem2  13836  pilem3  13837  coseq0negpitopi  13890  abssinper  13900  cos02pilt1  13905  relogeftb  13919  logbgcd1irraplemexp  14019  logbgcd1irrap  14021  lgsval  14038  lgsfvalg  14039  lgsfcl2  14040  lgsval2lem  14044  lgsmod  14060  lgsdilem  14061  lgsdir2lem4  14065  lgsdir2  14067  lgsdir  14069  lgsdilem2  14070  lgsdi  14071  lgsne0  14072  lgsdirnn0  14081  lgsdinn0  14082  2sqlem5  14088  2sqlem6  14089  2sqlem7  14090  2sqlem9  14093  2sqlem10  14094  bj-findis  14353  pwle2  14370  pwf1oexmid  14371  pw1nct  14375  nnsf  14377  peano4nninf  14378  nninfall  14381  nninfsellemeq  14386  nninfsellemeqinf  14388  qdencn  14398  refeq  14399  trilpolemeq1  14411  trilpolemlt1  14412  trirec0  14415  nconstwlpolemgt0  14434  nconstwlpolem  14435  neapmkvlem  14437
  Copyright terms: Public domain W3C validator