Theorem ad2antrr 492

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 481	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antrrr  496  ad5ant13  523  ad5ant23  526  simpll  531  simplll  539  simpllr  540  ad5ant123  1270  vtoclgft  2873  reupick  3517  ifeqeqxdc  3687  euotd  4395  frirrg  4495  ralxfrd  4608  nnsucpred  4764  foun  5658  f1oprg  5685  dffo4  5856  funopsn  5891  foeqcnvco  5996  fliftfun  6002  isotr  6022  riotass2  6067  ovmpodxf  6214  suppfnss  6497  suppcofn  6506  mpoxopoveq  6511  tfrlem1  6579  tfrlemibacc  6597  tfrlemibfn  6599  tfrlemi14d  6604  tfrexlem  6605  tfr1onlembacc  6613  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllembacc  6626  tfrcllembfn  6628  tfrcllemres  6633  frecabcl  6670  nnmordi  6789  eroprf  6902  mapsnd  6970  f1imaen2g  7080  pw2f1odclem  7134  xpen  7145  mapen  7146  mapdom1g  7147  mapxpen  7148  xpmapenlem  7149  phplem4dom  7163  nndomo  7165  phpm  7167  fidifsnen  7172  dif1enen  7184  fisbth  7187  fimax2gtrilemstep  7205  fimax2gtri  7206  eqsndc  7210  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  ssfirab  7244  fidcenumlemrks  7270  sbthlemi8  7281  fiuni  7312  2omap  7318  ordiso2  7375  updjud  7422  difinfsnlem  7439  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  enumct  7455  nnnninfeq  7468  nninfisol  7473  enomnilem  7478  fodju0  7487  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemg  7515  pr1or2  7540  pr2cv1  7541  exmidfodomrlemim  7553  exmidontriimlem2  7578  exmidapne  7626  cc3  7634  dfplpq2  7721  nqpi  7745  nqnq0pi  7805  nq0nn  7809  elinp  7841  elnp1st2nd  7843  genprndl  7888  genprndu  7889  addnqprllem  7894  addnqprulem  7895  addnqprl  7896  addnqpru  7897  addlocpr  7903  nqprloc  7912  prmuloc  7933  mulnqprl  7935  mulnqpru  7936  mullocpr  7938  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  archrecpr  8031  caucvgprlemnkj  8033  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemdisj  8069  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  mulgt0sr  8145  caucvgsrlemcau  8160  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axsuploc  8398  cnegexlem1  8501  cnegex  8504  apsym  8934  apcotr  8935  apadd1  8936  mulext1  8940  mulge0  8947  apti  8950  aprcl  8974  conjmulap  9059  lemulge11  9196  creui  9290  nndiv  9345  zaddcllemneg  9683  suprzclex  9744  eluzuzle  9930  infregelbex  9998  divfnzn  10021  qapne  10039  xrltso  10198  xnn0dcle  10204  xnn0letri  10205  xrre  10222  xrre3  10224  xaddf  10246  xaddval  10247  xpncan  10273  xleadd1a  10275  xltadd1  10278  xleaddadd  10289  ixxss12  10308  elioc2  10338  elico2  10339  elicc2  10340  fzm1  10507  fzneuz  10508  eluzgtdifelfzo  10615  elfzonelfzo  10648  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemex  10684  exbtwnz  10685  modqid  10786  modqcyc2  10797  modqmuladd  10803  modqmuladdnn0  10805  modaddmodlo  10825  addmodlteq  10835  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgsuc  10851  frecuzrdgsuctlem  10860  nninfinf  10880  seq3clss  10908  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemmo  10942  iseqf1olemqf1o  10943  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seq3f1olemp  10952  seq3f1oleml  10953  seq3f1o  10954  seqf1oglem1  10956  seqf1oglem2  10957  seqf1og  10958  seq3id3  10961  seqfeq4g  10968  ser3ge0  10973  exp3val  10978  expap0  11006  qsqeqor  11087  modqexp  11104  nn0ltexp2  11147  facndiv  11177  faclbnd  11179  bcval5  11201  hashunlem  11244  hashun  11245  hashprg  11249  fiprsshashgt1  11258  hashfacen  11284  hashf1lem1  11285  zfz1isolemiso  11291  zfz1isolem1  11292  seq3coll  11294  hashtpglem  11298  ccatcl  11361  ccatlen  11363  ccatvalfn  11369  ccatsymb  11370  ccatrn  11377  ccat2s1fstg  11416  swrdclg  11422  swrdspsleq  11439  pfxeq  11468  swrdswrd  11477  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12  11505  pfxccat3  11506  swrdccat3b  11512  reuccatpfxs1  11519  ovshftex  11584  2shfti  11596  seq3shft  11603  cjap  11672  caucvgrelemcau  11746  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniq  11761  resqrexlemdecn  11778  resqrexlemcalc3  11782  resqrexlemcvg  11785  resqrexlemoverl  11787  leabs  11840  absexpzap  11846  ltabs  11853  abslt  11854  absle  11855  maxleim  11971  maxabslemval  11974  fimaxre2  11993  minmax  11996  2zinfmin  12009  xrmaxiflemcl  12011  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  xrmaxltsup  12024  xrmaxadd  12027  xrminmax  12031  xrbdtri  12042  2clim  12067  climshftlemg  12068  climsqz  12101  climsqz2  12102  climrecvg1n  12114  climcvg1nlem  12115  serf0  12118  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  summodclem2  12149  zsumdc  12151  fsum3  12154  isumss  12158  fisumss  12159  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  fsumsplit  12174  sumsnf  12176  fsum2d  12202  fisum0diag2  12214  fsummulc2  12215  modfsummod  12225  fsumabs  12232  fsumrelem  12238  fsumiun  12244  geoisumr  12285  cvgratnnlemseq  12293  cvgratz  12299  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodrbdclem  12338  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  fprodssdc  12357  fprodmul  12358  prodsnf  12359  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  fprodcl2lem  12372  fprodap0  12388  fprod2d  12390  fprodrec  12396  fprodap0f  12403  efcj  12440  efaddlem  12441  tanaddaplem  12505  sinltxirr  12528  nndivides  12564  dvdsext  12622  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  bitsfzolem  12721  bitsmod  12723  bitsinv1  12729  dvdsbnd  12733  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemzz  12779  bezoutlemaz  12780  bezoutlembz  12781  bezoutlemeu  12784  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dfgcd2  12791  bezoutr1  12810  nnmindc  12811  nninfctlemfo  12817  dvdslcm  12847  lcmgcdlem  12855  qredeq  12874  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  isprm2lem  12894  prmind2  12898  exprmfct  12916  prmdvdsfz  12917  isprm5lem  12919  prmexpb  12929  rpexp1i  12932  sqrt2irr  12940  sqne2sq  12955  nonsq  12985  phiprmpw  13000  eulerthlemrprm  13007  eulerthlema  13008  hashgcdeq  13018  phisum  13019  modprmn0modprm0  13035  pclemub  13066  pclemdc  13067  pcmul  13080  pcqmul  13082  pcxqcl  13091  pcdvdstr  13106  pcprmpw2  13112  difsqpwdvds  13117  pcmpt  13122  oddprmdvds  13133  prmpwdvds  13134  pockthg  13136  infpnlem1  13138  1arith  13146  4sqlem2  13168  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  4sqlem11  13180  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemscl  13247  ballotfilemimin  13249  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsv  13253  ballotfilemsdom  13255  ballotfilemsima  13259  ennnfonelemg  13294  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemfun  13308  ennnfonelemf1  13309  ennnfonelemrn  13310  ennnfonelemdm  13311  ennnfonelemnn0  13313  ennnfonelemim  13315  exmidunben  13317  ctinfomlemom  13318  ctinf  13321  ctiunctlemudc  13328  nninfdclemlt  13342  nninfdclemf1  13343  isstruct2r  13363  imasival  13627  sgrppropd  13728  mndpropd  13753  issubmnd  13755  mndissubm  13782  resmhm2b  13796  mhmeql  13799  gzsumwsubmcl  13801  gzsumwmhm  13803  gzsumcl  13804  grpinvnz  13876  mhmmnd  13919  mulgfng  13927  mulgz  13953  mulgnndir  13954  mulgnn0dir  13955  mulgneg2  13959  mulgass  13962  mhmmulg  13966  issubgrpd2  13993  issubg4m  13996  grpissubg  13997  isnsg3  14010  ghmpreima  14069  ghmnsgpreima  14072  ghmf1  14076  conjnmz  14082  conjnmzb  14083  eqgabl  14134  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gsumvalfi  14152  gsumclfi  14159  gsumf1ofi  14160  gsummptfidmadd  14161  gsumsubmclfi  14163  prdsval  14173  prdssgrpd  14191  prdsidlem  14193  prdsmndd  14194  pws0g  14213  pwssub  14216  rngpropd  14254  issrg  14269  ringpropd  14343  ringinvnz1ne0  14354  dvdsrvald  14400  dvdsrd  14401  dvdsrtr  14408  unitgrp  14423  rhmopp  14483  aprnzr  14599  opprdrng  14620  lmodfopne  14663  lmodprop2d  14685  lssvacl  14702  lsslss  14718  lss1d  14720  lsspropdg  14768  rnglidlmcl  14817  lidlacl  14821  isridl  14841  gsumfsum  14923  znidomb  14993  znunit  14994  znrrg  14995  issubassa2  15035  psrval  15050  mplsubgfilemcl  15090  mplsubgfileminv  15091  mplsubgfi  15092  tgdom  15173  neipsm  15255  tgrest  15270  cnfval  15295  cnpfval  15296  cnpval  15299  iscnp4  15319  cnpnei  15320  cnptopco  15323  cncnpi  15329  cncnp  15331  cnptopresti  15339  cnptoprest2  15341  cndis  15342  lmtopcnp  15351  txbasval  15368  neitx  15369  txcnp  15372  txcnmpt  15374  txcn  15376  imasnopn  15400  psmetres2  15434  isxmet2d  15449  xblss2ps  15505  xblss2  15506  blbas  15534  neibl  15592  metss2lem  15598  metrest  15607  xmettx  15611  metcnp3  15612  metcnp  15613  metcnp2  15614  metcnpi  15616  metcnpi2  15617  mulc1cncf  15690  cncfco  15692  mulcncflem  15708  mulcncf  15709  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeu  15724  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemicc  15733  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthinc  15744  limcimolemlt  15765  limccnp2lem  15777  limccnp2cntop  15778  limccoap  15779  dvcj  15810  dvmptfsum  15826  dveflem  15827  plyf  15838  plyaddlem1  15848  plymullem1  15849  plycolemc  15859  plyco  15860  plycj  15862  dvply1  15866  dvply2g  15867  efltlemlt  15875  sin0pilem1  15882  sin0pilem2  15883  pilem3  15884  coseq0negpitopi  15937  abssinper  15947  cos02pilt1  15952  relogeftb  15966  logbgcd1irraplemexp  16070  logbgcd1irrap  16072  birthdaylem2  16088  dvdsppwf1o  16103  mpodvdsmulf1o  16104  mersenne  16111  perfectlem2  16114  perfect  16115  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsval2lem  16129  lgsmod  16145  lgsdilem  16146  lgsdir2lem4  16150  lgsdir2  16152  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  2lgslem1a1  16205  2lgslem1a  16207  2sqlem5  16238  2sqlem6  16239  2sqlem7  16240  2sqlem9  16243  2sqlem10  16244  umgrnloopv  16355  uhgr2edg  16447  upgredginwlk  16597  clwwlkccatlem  16641  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  eupth2lemsfi  16719  depindlem3  16749  bj-findis  17005  pwle2  17028  pwf1oexmid  17029  pw1nct  17033  wexmiddiffi  17044  nnsf  17048  peano4nninf  17049  nninfall  17052  nninfsellemeq  17057  nninfsellemeqinf  17059  nnnninfex  17065  nninfnfiinf  17066  qdencn  17072  refeq  17073  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  nconstwlpolemgt0  17114  nconstwlpolem  17115  neapmkvlem  17117