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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrr	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantlr 477	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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  ad5ant123  1242  vtoclgft  2825  reupick  3461  euotd  4306  frirrg  4404  ralxfrd  4516  nnsucpred  4672  foun  5552  f1oprg  5578  dffo4  5740  funopsn  5774  foeqcnvco  5871  fliftfun  5877  isotr  5897  riotass2  5938  ovmpodxf  6083  mpoxopoveq  6338  tfrlem1  6406  tfrlemibacc  6424  tfrlemibfn  6426  tfrlemi14d  6431  tfrexlem  6432  tfr1onlembacc  6440  tfr1onlembfn  6442  tfr1onlemres  6447  tfrcllembacc  6453  tfrcllembfn  6455  tfrcllemres  6460  frecabcl  6497  nnmordi  6614  eroprf  6727  f1imaen2g  6897  pw2f1odclem  6945  xpen  6956  mapen  6957  mapdom1g  6958  mapxpen  6959  xpmapenlem  6960  phplem4dom  6973  nndomo  6975  phpm  6976  fidifsnen  6981  dif1enen  6991  fisbth  6994  fimax2gtrilemstep  7011  fimax2gtri  7012  en2eqpr  7018  unsnfidcex  7031  unsnfidcel  7032  ssfirab  7047  fidcenumlemrks  7069  sbthlemi8  7080  fiuni  7094  ordiso2  7151  updjud  7198  difinfsnlem  7215  ctssdclemn0  7226  ctssdccl  7227  ctssdc  7229  enumctlemm  7230  enumct  7231  nnnninfeq  7244  nninfisol  7249  enomnilem  7254  fodju0  7263  enmkvlem  7277  enwomnilem  7285  nninfwlpoimlemg  7291  pr1or2  7315  exmidfodomrlemim  7324  exmidontriimlem2  7349  exmidapne  7387  cc3  7395  dfplpq2  7482  nqpi  7506  nqnq0pi  7566  nq0nn  7570  elinp  7602  elnp1st2nd  7604  genprndl  7649  genprndu  7650  addnqprllem  7655  addnqprulem  7656  addnqprl  7657  addnqpru  7658  addlocpr  7664  nqprloc  7673  prmuloc  7694  mulnqprl  7696  mulnqpru  7697  mullocpr  7699  distrlem1prl  7710  distrlem1pru  7711  ltsopr  7724  ltexprlemopl  7729  ltexprlemopu  7731  ltexprlemloc  7735  ltexprlemrl  7738  ltexprlemru  7740  addcanprleml  7742  addcanprlemu  7743  recexprlemloc  7759  recexprlem1ssl  7761  recexprlem1ssu  7762  aptiprleml  7767  aptiprlemu  7768  archpr  7771  cauappcvgprlemm  7773  cauappcvgprlemopl  7774  cauappcvgprlemlol  7775  cauappcvgprlemladdfu  7782  cauappcvgprlemladdfl  7783  cauappcvgprlemladdru  7784  archrecpr  7792  caucvgprlemnkj  7794  caucvgprlemm  7796  caucvgprlemopl  7797  caucvgprlemlol  7798  caucvgprlemdisj  7802  caucvgprlemloc  7803  caucvgprlemladdfu  7805  caucvgprprlemnkltj  7817  caucvgprprlemnkeqj  7818  caucvgprprlemnjltk  7819  caucvgprprlemml  7822  caucvgprprlemopl  7825  caucvgprprlemlol  7826  caucvgprprlemdisj  7830  caucvgprprlemexbt  7834  caucvgprprlemexb  7835  caucvgprprlemaddq  7836  suplocexprlemru  7847  suplocexprlemloc  7849  suplocexprlemex  7850  suplocexprlemub  7851  suplocexprlemlub  7852  mulgt0sr  7906  caucvgsrlemcau  7921  caucvgsrlemoffcau  7926  caucvgsrlemoffres  7928  suplocsrlemb  7934  suplocsrlempr  7935  suplocsrlem  7936  axcaucvglemcau  8026  axcaucvglemres  8027  axpre-suploclemres  8029  axsuploc  8160  cnegexlem1  8262  cnegex  8265  apsym  8694  apcotr  8695  apadd1  8696  mulext1  8700  mulge0  8707  apti  8710  aprcl  8734  conjmulap  8817  lemulge11  8954  creui  9048  nndiv  9092  zaddcllemneg  9426  suprzclex  9486  eluzuzle  9671  infregelbex  9734  divfnzn  9757  qapne  9775  xrltso  9933  xnn0dcle  9939  xnn0letri  9940  xrre  9957  xrre3  9959  xaddf  9981  xaddval  9982  xpncan  10008  xleadd1a  10010  xltadd1  10013  xleaddadd  10024  ixxss12  10043  elioc2  10073  elico2  10074  elicc2  10075  fzm1  10237  fzneuz  10238  eluzgtdifelfzo  10343  elfzonelfzo  10376  exfzdc  10386  zsupcllemstep  10389  infssuzex  10393  suprzubdc  10396  nninfdcex  10397  zsupssdc  10398  qtri3or  10400  exbtwnzlemstep  10407  exbtwnzlemex  10409  exbtwnz  10410  modqid  10511  modqcyc2  10522  modqmuladd  10528  modqmuladdnn0  10530  modaddmodlo  10550  addmodlteq  10560  frecuzrdgrrn  10570  frec2uzrdg  10571  frecuzrdgsuc  10576  frecuzrdgsuctlem  10585  nninfinf  10605  seq3clss  10633  iseqf1olemqcl  10661  iseqf1olemnab  10663  iseqf1olemab  10664  iseqf1olemmo  10667  iseqf1olemqf1o  10668  iseqf1olemjpcl  10670  iseqf1olemqpcl  10671  seq3f1olemqsumk  10674  seq3f1olemqsum  10675  seq3f1olemp  10677  seq3f1oleml  10678  seq3f1o  10679  seqf1oglem1  10681  seqf1oglem2  10682  seqf1og  10683  seq3id3  10686  seqfeq4g  10693  ser3ge0  10698  exp3val  10703  expap0  10731  qsqeqor  10812  modqexp  10828  nn0ltexp2  10871  facndiv  10901  faclbnd  10903  bcval5  10925  hashunlem  10966  hashun  10967  hashprg  10970  fiprsshashgt1  10979  hashfacen  10998  zfz1isolemiso  11001  zfz1isolem1  11002  seq3coll  11004  ccatcl  11067  ccatlen  11069  ccatvalfn  11075  ccatsymb  11076  ccatrn  11083  swrdclg  11121  swrdspsleq  11138  pfxeq  11167  swrdswrd  11176  wrdind  11193  wrd2ind  11194  ovshftex  11200  2shfti  11212  seq3shft  11219  cjap  11287  caucvgrelemcau  11361  cvg1nlemcau  11365  cvg1nlemres  11366  recvguniq  11376  resqrexlemdecn  11393  resqrexlemcalc3  11397  resqrexlemcvg  11400  resqrexlemoverl  11402  leabs  11455  absexpzap  11461  ltabs  11468  abslt  11469  absle  11470  maxleim  11586  maxabslemval  11589  fimaxre2  11608  minmax  11611  2zinfmin  11624  xrmaxiflemcl  11626  xrmaxifle  11627  xrmaxiflemab  11628  xrmaxiflemlub  11629  xrmaxiflemcom  11630  xrmaxltsup  11639  xrmaxadd  11642  xrminmax  11646  xrbdtri  11657  2clim  11682  climshftlemg  11683  climsqz  11716  climsqz2  11717  climrecvg1n  11729  climcvg1nlem  11730  serf0  11733  sumrbdclem  11758  fsum3cvg  11759  summodclem3  11761  summodclem2a  11762  summodclem2  11763  zsumdc  11765  fsum3  11768  isumss  11772  fisumss  11773  fsum3cvg3  11777  fsumcl2lem  11779  fsumadd  11787  fsumsplit  11788  sumsnf  11790  fsum2d  11816  fisum0diag2  11828  fsummulc2  11829  modfsummod  11839  fsumabs  11846  fsumrelem  11852  fsumiun  11858  geoisumr  11899  cvgratnnlemseq  11907  cvgratz  11913  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  prodrbdclem  11952  fproddccvg  11953  prodmodclem3  11956  prodmodclem2a  11957  zproddc  11960  fprodseq  11964  fprodntrivap  11965  fprodssdc  11971  fprodmul  11972  prodsnf  11973  fprodsplitdc  11977  fprodsplit  11978  fprodunsn  11985  fprodcl2lem  11986  fprodap0  12002  fprod2d  12004  fprodrec  12010  fprodap0f  12017  efcj  12054  efaddlem  12055  tanaddaplem  12119  sinltxirr  12142  nndivides  12178  dvdsext  12236  divalglemeunn  12302  divalglemex  12303  divalglemeuneg  12304  bitsfzolem  12335  bitsmod  12337  bitsinv1  12343  dvdsbnd  12347  bezoutlemnewy  12387  bezoutlemstep  12388  bezoutlemmain  12389  bezoutlemzz  12393  bezoutlemaz  12394  bezoutlembz  12395  bezoutlemeu  12398  bezoutlemle  12399  bezoutlemsup  12400  dfgcd3  12401  dfgcd2  12405  bezoutr1  12424  nnmindc  12425  nninfctlemfo  12431  dvdslcm  12461  lcmgcdlem  12469  qredeq  12488  qredeu  12489  divgcdcoprm0  12493  divgcdcoprmex  12494  cncongr1  12495  isprm2lem  12508  prmind2  12512  exprmfct  12530  prmdvdsfz  12531  isprm5lem  12533  prmexpb  12543  rpexp1i  12546  sqrt2irr  12554  sqne2sq  12569  nonsq  12599  phiprmpw  12614  eulerthlemrprm  12621  eulerthlema  12622  hashgcdeq  12632  phisum  12633  modprmn0modprm0  12649  pclemub  12680  pclemdc  12681  pcmul  12694  pcqmul  12696  pcxqcl  12705  pcdvdstr  12720  pcprmpw2  12726  difsqpwdvds  12731  pcmpt  12736  oddprmdvds  12747  prmpwdvds  12748  pockthg  12750  infpnlem1  12752  1arith  12760  4sqlem2  12782  4sqlemafi  12788  4sqlemffi  12789  4sqleminfi  12790  4sqlem11  12794  4sqlem13m  12796  4sqlem14  12797  4sqlem17  12800  4sqlem18  12801  ennnfonelemg  12844  ennnfoneleminc  12852  ennnfonelemkh  12853  ennnfonelemhf1o  12854  ennnfonelemex  12855  ennnfonelemhom  12856  ennnfonelemfun  12858  ennnfonelemf1  12859  ennnfonelemrn  12860  ennnfonelemdm  12861  ennnfonelemnn0  12863  ennnfonelemim  12865  exmidunben  12867  ctinfomlemom  12868  ctinf  12871  ctiunctlemudc  12878  nninfdclemlt  12892  nninfdclemf1  12893  isstruct2r  12913  prdsval  13175  imasival  13208  gsumpropd2  13295  sgrppropd  13315  prdssgrpd  13317  mndpropd  13342  issubmnd  13344  prdsidlem  13349  prdsmndd  13350  pws0g  13353  mndissubm  13377  resmhm2b  13391  mhmeql  13394  gsumfzz  13397  gsumwsubmcl  13398  gsumwmhm  13400  gsumfzcl  13401  grpinvnz  13473  pwssub  13515  mhmmnd  13522  mulgfng  13530  mulgz  13556  mulgnndir  13557  mulgnn0dir  13558  mulgneg2  13562  mulgass  13565  mhmmulg  13569  issubgrpd2  13596  issubg4m  13599  grpissubg  13600  isnsg3  13613  ghmpreima  13672  ghmnsgpreima  13675  ghmf1  13679  conjnmz  13685  conjnmzb  13686  eqgabl  13736  gsumfzreidx  13743  gsumfzsubmcl  13744  gsumfzmptfidmadd  13745  gsumfzmhm  13749  rngpropd  13787  issrg  13797  ringpropd  13870  ringinvnz1ne0  13881  dvdsrvald  13925  dvdsrd  13926  dvdsrtr  13933  unitgrp  13948  rhmopp  14008  lmodfopne  14158  lmodprop2d  14180  lssvacl  14197  lsslss  14213  lss1d  14215  lsspropdg  14263  rnglidlmcl  14312  lidlacl  14316  isridl  14336  znidomb  14490  znunit  14491  znrrg  14492  psrval  14498  mplsubgfilemcl  14531  mplsubgfileminv  14532  mplsubgfi  14533  tgdom  14614  neipsm  14696  tgrest  14711  cnfval  14736  cnpfval  14737  cnpval  14740  iscnp4  14760  cnpnei  14761  cnptopco  14764  cncnpi  14770  cncnp  14772  cnptopresti  14780  cnptoprest2  14782  cndis  14783  lmtopcnp  14792  txbasval  14809  neitx  14810  txcnp  14813  txcnmpt  14815  txcn  14817  imasnopn  14841  psmetres2  14875  isxmet2d  14890  xblss2ps  14946  xblss2  14947  blbas  14975  neibl  15033  metss2lem  15039  metrest  15048  xmettx  15052  metcnp3  15053  metcnp  15054  metcnp2  15055  metcnpi  15057  metcnpi2  15058  mulc1cncf  15131  cncfco  15133  mulcncflem  15149  mulcncf  15150  dedekindeulemuub  15159  dedekindeulemloc  15161  dedekindeulemlu  15163  dedekindeu  15165  suplociccreex  15166  suplociccex  15167  dedekindicclemuub  15168  dedekindicclemloc  15170  dedekindicclemlu  15172  dedekindicclemicc  15174  dedekindicc  15175  ivthinclemlopn  15178  ivthinclemlr  15179  ivthinclemuopn  15180  ivthinclemur  15181  ivthinclemloc  15183  ivthinc  15185  limcimolemlt  15206  limccnp2lem  15218  limccnp2cntop  15219  limccoap  15220  dvcj  15251  dvmptfsum  15267  dveflem  15268  plyf  15279  plyaddlem1  15289  plymullem1  15290  plycolemc  15300  plyco  15301  plycj  15303  dvply1  15307  dvply2g  15308  efltlemlt  15316  sin0pilem1  15323  sin0pilem2  15324  pilem3  15325  coseq0negpitopi  15378  abssinper  15388  cos02pilt1  15393  relogeftb  15407  logbgcd1irraplemexp  15510  logbgcd1irrap  15512  dvdsppwf1o  15531  mpodvdsmulf1o  15532  mersenne  15539  perfectlem2  15542  perfect  15543  lgsval  15551  lgsfvalg  15552  lgsfcl2  15553  lgsval2lem  15557  lgsmod  15573  lgsdilem  15574  lgsdir2lem4  15578  lgsdir2  15580  lgsdir  15582  lgsdilem2  15583  lgsdi  15584  lgsne0  15585  lgsdirnn0  15594  lgsdinn0  15595  gausslemma2dlem1a  15605  gausslemma2dlem1f1o  15607  lgsquadlem1  15624  lgsquadlem2  15625  lgsquad2lem2  15629  2lgslem1a1  15633  2lgslem1a  15635  2sqlem5  15666  2sqlem6  15667  2sqlem7  15668  2sqlem9  15671  2sqlem10  15672  umgrnloopvv  15780  bj-findis  16049  2omap  16067  pwle2  16070  pwf1oexmid  16071  pw1nct  16075  nnsf  16077  peano4nninf  16078  nninfall  16081  nninfsellemeq  16086  nninfsellemeqinf  16088  nnnninfex  16094  nninfnfiinf  16095  qdencn  16101  refeq  16102  trilpolemeq1  16114  trilpolemlt1  16115  trirec0  16118  nconstwlpolemgt0  16138  nconstwlpolem  16139  neapmkvlem  16141