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  8502  cnegex  8505  apsym  8936  apcotr  8937  apadd1  8938  mulext1  8942  mulge0  8949  apti  8952  aprcl  8976  conjmulap  9061  lemulge11  9198  creui  9292  nndiv  9347  zaddcllemneg  9687  suprzclex  9748  eluzuzle  9939  infregelbex  10007  divfnzn  10030  qapne  10048  xrltso  10208  xnn0dcle  10214  xnn0letri  10215  xrre  10232  xrre3  10234  xaddf  10256  xaddval  10257  xpncan  10283  xleadd1a  10285  xltadd1  10288  xleaddadd  10299  ixxss12  10318  elioc2  10348  elico2  10349  elicc2  10350  fzm1  10517  fzneuz  10518  eluzgtdifelfzo  10625  elfzonelfzo  10658  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemex  10694  exbtwnz  10695  modqid  10799  modqcyc2  10810  modqmuladd  10816  modqmuladdnn0  10818  modaddmodlo  10838  addmodlteq  10848  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgsuc  10864  frecuzrdgsuctlem  10873  nninfinf  10893  seq3clss  10921  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemmo  10955  iseqf1olemqf1o  10956  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seq3f1olemp  10965  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem1  10969  seqf1oglem2  10970  seqf1og  10971  seq3id3  10974  seqfeq4g  10981  ser3ge0  10986  exp3val  10991  expap0  11019  qsqeqor  11100  modqexp  11117  nn0sqdc  11160  nn0ltexp2  11161  facndiv  11191  faclbnd  11193  bcval5  11215  hashunlem  11258  hashun  11259  hashprg  11263  fiprsshashgt1  11272  hashfacen  11298  hashf1lem1  11299  zfz1isolemiso  11305  zfz1isolem1  11306  seq3coll  11308  hashtpglem  11312  ccatcl  11375  ccatlen  11377  ccatvalfn  11383  ccatsymb  11384  ccatrn  11391  ccat2s1fstg  11430  swrdclg  11436  swrdspsleq  11453  pfxeq  11482  swrdswrd  11491  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12  11519  pfxccat3  11520  swrdccat3b  11526  reuccatpfxs1  11533  ovshftex  11598  2shfti  11610  seq3shft  11617  cjap  11686  caucvgrelemcau  11760  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniq  11775  resqrexlemdecn  11792  resqrexlemcalc3  11796  resqrexlemcvg  11799  resqrexlemoverl  11801  leabs  11854  absexpzap  11861  ltabs  11868  abslt  11869  absle  11870  maxleim  11986  maxabslemval  11989  fimaxre2  12008  minmax  12011  2zinfmin  12025  xrmaxiflemcl  12027  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  xrmaxltsup  12040  xrmaxadd  12043  xrminmax  12047  xrbdtri  12058  2clim  12083  climshftlemg  12084  climsqz  12117  climsqz2  12118  climrecvg1n  12130  climcvg1nlem  12131  serf0  12134  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  summodclem2  12165  zsumdc  12167  fsum3  12170  isumss  12174  fisumss  12175  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  fsumsplit  12190  sumsnf  12192  fsum2d  12218  fisum0diag2  12230  fsummulc2  12231  modfsummod  12241  fsumabs  12248  fsumrelem  12254  fsumiun  12260  geoisumr  12301  cvgratnnlemseq  12309  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodntrivap  12367  fprodssdc  12373  fprodmul  12374  prodsnf  12375  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  fprodcl2lem  12388  fprodap0  12404  fprod2d  12406  fprodrec  12412  fprodap0f  12419  efcj  12456  efaddlem  12457  tanaddaplem  12521  sinltxirr  12544  nndivides  12580  dvdsext  12638  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  bitsfzolem  12737  bitsmod  12739  bitsinv1  12745  dvdsbnd  12749  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemzz  12795  bezoutlemaz  12796  bezoutlembz  12797  bezoutlemeu  12800  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dfgcd2  12807  bezoutr1  12826  nnmindc  12827  nninfctlemfo  12833  dvdslcm  12863  lcmgcdlem  12871  qredeq  12890  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  isprm2lem  12910  prmind2  12914  exprmfct  12933  prmdvdsfz  12934  isprm5lem  12936  prmexpb  12946  rpexp1i  12949  sqrt2irr  12957  pwbdvdslemn  12960  sqne2sq  12973  nonsq  13003  phiprmpw  13020  eulerthlemrprm  13027  eulerthlema  13028  hashgcdeq  13038  phisum  13039  modprmn0modprm0  13055  pclemub  13086  pclemdc  13087  pcmul  13100  pcqmul  13102  pcxqcl  13111  pcdvdstr  13126  pcprmpw2  13132  difsqpwdvds  13137  pcmpt  13142  oddprmdvds  13153  prmpwdvds  13154  pockthg  13156  infpnlem1  13158  1arith  13166  4sqlem2  13188  4sqlemafi  13194  4sqlemffi  13195  4sqleminfi  13196  4sqlem11  13200  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemscl  13296  ballotfilemimin  13298  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsv  13302  ballotfilemsdom  13304  ballotfilemsima  13308  ennnfonelemg  13343  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemfun  13357  ennnfonelemf1  13358  ennnfonelemrn  13359  ennnfonelemdm  13360  ennnfonelemnn0  13362  ennnfonelemim  13364  exmidunben  13366  ctinfomlemom  13367  ctinf  13370  ctiunctlemudc  13377  nninfdclemlt  13391  nninfdclemf1  13392  isstruct2r  13412  imasival  13676  sgrppropd  13777  mndpropd  13802  issubmnd  13804  mndissubm  13831  resmhm2b  13845  mhmeql  13848  gzsumwsubmcl  13850  gzsumwmhm  13852  gzsumcl  13853  grpinvnz  13925  mhmmnd  13968  mulgfng  13976  mulgz  14002  mulgnndir  14003  mulgnn0dir  14004  mulgneg2  14008  mulgass  14011  mhmmulg  14015  issubgrpd2  14042  issubg4m  14045  grpissubg  14046  isnsg3  14059  ghmpreima  14118  ghmnsgpreima  14121  ghmf1  14125  conjnmz  14131  conjnmzb  14132  eqgabl  14183  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gsumvalfi  14201  gsumclfi  14208  gsumf1ofi  14209  gsummptfidmadd  14210  gsumsubmclfi  14212  prdsval  14222  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  pws0g  14262  pwssub  14265  rngpropd  14303  issrg  14318  ringpropd  14392  ringinvnz1ne0  14403  dvdsrvald  14449  dvdsrd  14450  dvdsrtr  14457  unitgrp  14472  rhmopp  14532  aprnzr  14648  opprdrng  14669  lmodfopne  14712  lmodprop2d  14734  lssvacl  14751  lsslss  14767  lss1d  14769  lsspropdg  14817  rnglidlmcl  14866  lidlacl  14870  isridl  14890  gsumfsum  14972  znidomb  15042  znunit  15043  znrrg  15044  issubassa2  15084  psrval  15099  mplsubgfilemcl  15139  mplsubgfileminv  15140  mplsubgfi  15141  tgdom  15222  neipsm  15304  tgrest  15319  cnfval  15344  cnpfval  15345  cnpval  15348  iscnp4  15368  cnpnei  15369  cnptopco  15372  cncnpi  15378  cncnp  15380  cnptopresti  15388  cnptoprest2  15390  cndis  15391  lmtopcnp  15400  txbasval  15417  neitx  15418  txcnp  15421  txcnmpt  15423  txcn  15425  imasnopn  15449  psmetres2  15483  isxmet2d  15498  xblss2ps  15554  xblss2  15555  blbas  15583  neibl  15641  metss2lem  15647  metrest  15656  xmettx  15660  metcnp3  15661  metcnp  15662  metcnp2  15663  metcnpi  15665  metcnpi2  15666  mulc1cncf  15739  cncfco  15741  mulcncflem  15757  mulcncf  15758  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeu  15773  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemicc  15782  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthinc  15793  limcimolemlt  15814  limccnp2lem  15826  limccnp2cntop  15827  limccoap  15828  dvcj  15859  dvmptfsum  15875  dveflem  15876  plyf  15887  plyaddlem1  15897  plymullem1  15898  plycolemc  15908  plyco  15909  plycj  15911  dvply1  15915  dvply2g  15916  efltlemlt  15924  efap1p  15929  sin0pilem1  15932  sin0pilem2  15933  pilem3  15934  coseq0negpitopi  15987  abssinper  15997  cos02pilt1  16002  relogeftb  16016  logdivlt  16046  logbgcd1irraplemexp  16123  logbgcd1irrap  16125  birthdaylem2  16145  ppiqltx  16183  dvdsppwf1o  16184  mpodvdsmulf1o  16185  ppiqub  16194  mersenne  16195  perfectlem2  16198  perfect  16199  pcbcctr  16201  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsval2lem  16227  lgsmod  16243  lgsdilem  16244  lgsdir2lem4  16248  lgsdir2  16250  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  2lgslem1a1  16303  2lgslem1a  16305  2sqlem5  16336  2sqlem6  16337  2sqlem7  16338  2sqlem9  16341  2sqlem10  16342  umgrnloopv  16453  uhgr2edg  16545  upgredginwlk  16695  clwwlkccatlem  16739  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  eupth2lemsfi  16817  depindlem3  16847  bj-findis  17103  pwle2  17126  pwf1oexmid  17127  pw1nct  17131  wexmiddiffi  17142  nnsf  17146  peano4nninf  17147  nninfall  17150  nninfsellemeq  17155  nninfsellemeqinf  17157  nnnninfex  17163  nninfnfiinf  17164  qdencn  17170  refeq  17171  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  nconstwlpolemgt0  17212  nconstwlpolem  17213  neapmkvlem  17215