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

Theorem ad2antrr 477
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 (𝜑𝜓)
Assertion
Ref Expression
ad2antrr (((𝜑𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 272 . 2 ((𝜑𝜃) → 𝜓)
32adantlr 466 1 (((𝜑𝜒) ∧ 𝜃) → 𝜓)
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:  ad3antrrr  481  simpll  501  simplll  505  simpllr  506  vtoclgft  2708  reupick  3328  euotd  4144  frirrg  4240  ralxfrd  4351  nnsucpred  4498  foun  5352  f1oprg  5377  dffo4  5534  foeqcnvco  5657  fliftfun  5663  isotr  5683  riotass2  5722  ovmpodxf  5862  mpoxopoveq  6103  tfrlem1  6171  tfrlemibacc  6189  tfrlemibfn  6191  tfrlemi14d  6196  tfrexlem  6197  tfr1onlembacc  6205  tfr1onlembfn  6207  tfr1onlemres  6212  tfrcllembacc  6218  tfrcllembfn  6220  tfrcllemres  6225  frecabcl  6262  nnmordi  6378  eroprf  6488  f1imaen2g  6653  xpen  6705  mapen  6706  mapdom1g  6707  mapxpen  6708  xpmapenlem  6709  phplem4dom  6722  nndomo  6724  phpm  6725  fidifsnen  6730  dif1enen  6740  fisbth  6743  fimax2gtrilemstep  6760  fimax2gtri  6761  en2eqpr  6767  unsnfidcex  6774  unsnfidcel  6775  ssfirab  6788  fidcenumlemrks  6807  sbthlemi8  6818  fiuni  6832  ordiso2  6886  updjud  6933  difinfsnlem  6950  ctssdclemn0  6961  ctssdccl  6962  ctssdc  6964  enumctlemm  6965  enumct  6966  enomnilem  6976  fodju0  6985  exmidfodomrlemim  7021  dfplpq2  7126  nqpi  7150  nqnq0pi  7210  nq0nn  7214  elinp  7246  elnp1st2nd  7248  genprndl  7293  genprndu  7294  addnqprllem  7299  addnqprulem  7300  addnqprl  7301  addnqpru  7302  addlocpr  7308  nqprloc  7317  prmuloc  7338  mulnqprl  7340  mulnqpru  7341  mullocpr  7343  distrlem1prl  7354  distrlem1pru  7355  ltsopr  7368  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemloc  7379  ltexprlemrl  7382  ltexprlemru  7384  addcanprleml  7386  addcanprlemu  7387  recexprlemloc  7403  recexprlem1ssl  7405  recexprlem1ssu  7406  aptiprleml  7411  aptiprlemu  7412  archpr  7415  cauappcvgprlemm  7417  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlemladdru  7428  archrecpr  7436  caucvgprlemnkj  7438  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprprlemnkltj  7461  caucvgprprlemnkeqj  7462  caucvgprprlemnjltk  7463  caucvgprprlemml  7466  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemdisj  7474  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgprprlemaddq  7480  suplocexprlemru  7491  suplocexprlemloc  7493  suplocexprlemex  7494  suplocexprlemub  7495  suplocexprlemlub  7496  mulgt0sr  7550  caucvgsrlemcau  7565  caucvgsrlemoffcau  7570  caucvgsrlemoffres  7572  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  axsuploc  7801  cnegexlem1  7901  cnegex  7904  apsym  8331  apcotr  8332  apadd1  8333  mulext1  8337  mulge0  8344  apti  8347  aprcl  8370  conjmulap  8449  lemulge11  8581  creui  8675  nndiv  8718  zaddcllemneg  9044  suprzclex  9100  eluzuzle  9283  divfnzn  9362  qapne  9380  xrltso  9522  xrre  9543  xrre3  9545  xaddf  9567  xaddval  9568  xpncan  9594  xleadd1a  9596  xltadd1  9599  xleaddadd  9610  ixxss12  9629  elioc2  9659  elico2  9660  elicc2  9661  fzm1  9820  fzneuz  9821  eluzgtdifelfzo  9914  elfzonelfzo  9947  exfzdc  9957  qtri3or  9960  exbtwnzlemstep  9965  exbtwnzlemex  9967  exbtwnz  9968  modqid  10062  modqcyc2  10073  modqmuladd  10079  modqmuladdnn0  10081  modaddmodlo  10101  addmodlteq  10111  frecuzrdgrrn  10121  frec2uzrdg  10122  frecuzrdgsuc  10127  frecuzrdgsuctlem  10136  seq3clss  10180  iseqf1olemqcl  10199  iseqf1olemnab  10201  iseqf1olemab  10202  iseqf1olemmo  10205  iseqf1olemqf1o  10206  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  seq3f1olemqsumk  10212  seq3f1olemqsum  10213  seq3f1olemp  10215  seq3f1oleml  10216  seq3f1o  10217  seq3id3  10220  ser3ge0  10230  exp3val  10235  expap0  10263  facndiv  10425  faclbnd  10427  bcval5  10449  hashunlem  10490  hashun  10491  hashprg  10494  fiprsshashgt1  10503  hashfacen  10519  zfz1isolemiso  10522  zfz1isolem1  10523  seq3coll  10525  ovshftex  10531  2shfti  10543  seq3shft  10550  cjap  10618  caucvgrelemcau  10692  cvg1nlemcau  10696  cvg1nlemres  10697  recvguniq  10707  resqrexlemdecn  10724  resqrexlemcalc3  10728  resqrexlemcvg  10731  resqrexlemoverl  10733  leabs  10786  absexpzap  10792  ltabs  10799  abslt  10800  absle  10801  maxleim  10917  maxabslemval  10920  fimaxre2  10938  minmax  10941  xrmaxiflemcl  10954  xrmaxifle  10955  xrmaxiflemab  10956  xrmaxiflemlub  10957  xrmaxiflemcom  10958  xrmaxltsup  10967  xrmaxadd  10970  xrminmax  10974  xrbdtri  10985  2clim  11010  climshftlemg  11011  climsqz  11044  climsqz2  11045  climrecvg1n  11057  climcvg1nlem  11058  serf0  11061  sumrbdclem  11085  fsum3cvg  11086  summodclem3  11089  summodclem2a  11090  summodclem2  11091  zsumdc  11093  fsum3  11096  isumss  11100  fisumss  11101  fsum3cvg3  11105  fsumcl2lem  11107  fsumadd  11115  fsumsplit  11116  sumsnf  11118  fsum2d  11144  fisum0diag2  11156  fsummulc2  11157  modfsummod  11167  fsumabs  11174  fsumrelem  11180  fsumiun  11186  geoisumr  11227  cvgratnnlemseq  11235  cvgratz  11241  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  efcj  11278  efaddlem  11279  tanaddaplem  11344  nndivides  11396  dvdsext  11449  divalglemeunn  11514  divalglemex  11515  divalglemeuneg  11516  zsupcllemstep  11534  infssuzex  11538  dvdsbnd  11541  bezoutlemnewy  11580  bezoutlemstep  11581  bezoutlemmain  11582  bezoutlemzz  11586  bezoutlemaz  11587  bezoutlembz  11588  bezoutlemeu  11591  bezoutlemle  11592  bezoutlemsup  11593  dfgcd3  11594  dfgcd2  11598  bezoutr1  11617  dvdslcm  11646  lcmgcdlem  11654  qredeq  11673  qredeu  11674  divgcdcoprm0  11678  divgcdcoprmex  11679  cncongr1  11680  isprm2lem  11693  prmind2  11697  exprmfct  11714  prmdvdsfz  11715  prmexpb  11725  rpexp1i  11728  sqrt2irr  11736  sqne2sq  11750  nonsq  11780  phiprmpw  11793  hashgcdeq  11799  ennnfonelemg  11811  ennnfoneleminc  11819  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemfun  11825  ennnfonelemf1  11826  ennnfonelemrn  11827  ennnfonelemdm  11828  ennnfonelemnn0  11830  ennnfonelemim  11832  exmidunben  11834  ctinfomlemom  11835  ctinf  11838  ctiunctlemudc  11845  isstruct2r  11865  tgdom  12136  neipsm  12218  tgrest  12233  cnfval  12258  cnpfval  12259  cnpval  12262  iscnp4  12282  cnpnei  12283  cnptopco  12286  cncnpi  12292  cncnp  12294  cnptopresti  12302  cnptoprest2  12304  cndis  12305  lmtopcnp  12314  txbasval  12331  neitx  12332  txcnp  12335  txcnmpt  12337  txcn  12339  imasnopn  12363  psmetres2  12397  isxmet2d  12412  xblss2ps  12468  xblss2  12469  blbas  12497  neibl  12555  metss2lem  12561  metrest  12570  xmettx  12574  metcnp3  12575  metcnp  12576  metcnp2  12577  metcnpi  12579  metcnpi2  12580  mulc1cncf  12640  cncfco  12642  mulcncflem  12654  mulcncf  12655  dedekindeulemuub  12659  dedekindeulemloc  12661  dedekindeulemlu  12663  dedekindeu  12665  suplociccreex  12666  suplociccex  12667  dedekindicclemuub  12668  dedekindicclemloc  12670  dedekindicclemlu  12672  dedekindicclemicc  12674  dedekindicc  12675  ivthinclemlopn  12678  ivthinclemlr  12679  ivthinclemuopn  12680  ivthinclemur  12681  ivthinclemloc  12683  ivthinc  12685  limcimolemlt  12697  limccnp2lem  12709  limccnp2cntop  12710  limccoap  12711  dvcj  12737  dveflem  12750  bj-findis  13000  pwle2  13016  pwf1oexmid  13017  nnsf  13022  peano4nninf  13023  nninfalllemn  13025  nninfall  13027  nninfsellemeq  13033  nninfsellemeqinf  13035  qdencn  13045  refeq  13046  trilpolemeq1  13056  trilpolemlt1  13057
  Copyright terms: Public domain W3C validator