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  535  simpllr  536  ad5ant123  1266  vtoclgft  2867  reupick  3509  ifeqeqxdc  3673  euotd  4376  frirrg  4476  ralxfrd  4588  nnsucpred  4744  foun  5638  f1oprg  5665  dffo4  5830  funopsn  5865  foeqcnvco  5969  fliftfun  5975  isotr  5995  riotass2  6040  ovmpodxf  6187  suppfnss  6470  suppcofn  6479  mpoxopoveq  6484  tfrlem1  6552  tfrlemibacc  6570  tfrlemibfn  6572  tfrlemi14d  6577  tfrexlem  6578  tfr1onlembacc  6586  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllembacc  6599  tfrcllembfn  6601  tfrcllemres  6606  frecabcl  6643  nnmordi  6762  eroprf  6875  mapsnd  6936  f1imaen2g  7046  pw2f1odclem  7100  xpen  7111  mapen  7112  mapdom1g  7113  mapxpen  7114  xpmapenlem  7115  phplem4dom  7129  nndomo  7131  phpm  7133  fidifsnen  7138  dif1enen  7150  fisbth  7153  fimax2gtrilemstep  7171  fimax2gtri  7172  eqsndc  7176  en2eqpr  7180  unsnfidcex  7193  unsnfidcel  7194  ssfirab  7210  fidcenumlemrks  7236  sbthlemi8  7247  fiuni  7278  2omap  7282  ordiso2  7339  updjud  7386  difinfsnlem  7403  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  enumct  7419  nnnninfeq  7432  nninfisol  7437  enomnilem  7442  fodju0  7451  enmkvlem  7465  enwomnilem  7473  nninfwlpoimlemg  7479  pr1or2  7504  pr2cv1  7505  exmidfodomrlemim  7517  exmidontriimlem2  7542  exmidapne  7590  cc3  7598  dfplpq2  7685  nqpi  7709  nqnq0pi  7769  nq0nn  7773  elinp  7805  elnp1st2nd  7807  genprndl  7852  genprndu  7853  addnqprllem  7858  addnqprulem  7859  addnqprl  7860  addnqpru  7861  addlocpr  7867  nqprloc  7876  prmuloc  7897  mulnqprl  7899  mulnqpru  7900  mullocpr  7902  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  archrecpr  7995  caucvgprlemnkj  7997  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemdisj  8033  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  suplocexprlemlub  8055  mulgt0sr  8109  caucvgsrlemcau  8124  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axsuploc  8362  cnegexlem1  8464  cnegex  8467  apsym  8897  apcotr  8898  apadd1  8899  mulext1  8903  mulge0  8910  apti  8913  aprcl  8937  conjmulap  9020  lemulge11  9157  creui  9251  nndiv  9295  zaddcllemneg  9633  suprzclex  9694  eluzuzle  9880  infregelbex  9948  divfnzn  9971  qapne  9989  xrltso  10148  xnn0dcle  10154  xnn0letri  10155  xrre  10172  xrre3  10174  xaddf  10196  xaddval  10197  xpncan  10223  xleadd1a  10225  xltadd1  10228  xleaddadd  10239  ixxss12  10258  elioc2  10288  elico2  10289  elicc2  10290  fzm1  10456  fzneuz  10457  eluzgtdifelfzo  10564  elfzonelfzo  10597  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  modqid  10735  modqcyc2  10746  modqmuladd  10752  modqmuladdnn0  10754  modaddmodlo  10774  addmodlteq  10784  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgsuc  10800  frecuzrdgsuctlem  10809  nninfinf  10829  seq3clss  10857  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemmo  10891  iseqf1olemqf1o  10892  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  seq3id3  10910  seqfeq4g  10917  ser3ge0  10922  exp3val  10927  expap0  10955  qsqeqor  11036  modqexp  11053  nn0ltexp2  11096  facndiv  11126  faclbnd  11128  bcval5  11150  hashunlem  11193  hashun  11194  hashprg  11198  fiprsshashgt1  11207  hashfacen  11233  zfz1isolemiso  11236  zfz1isolem1  11237  seq3coll  11239  hashtpglem  11243  ccatcl  11306  ccatlen  11308  ccatvalfn  11314  ccatsymb  11315  ccatrn  11322  ccat2s1fstg  11361  swrdclg  11367  swrdspsleq  11384  pfxeq  11413  swrdswrd  11422  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12  11450  pfxccat3  11451  swrdccat3b  11457  reuccatpfxs1  11464  ovshftex  11529  2shfti  11541  seq3shft  11548  cjap  11616  caucvgrelemcau  11690  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniq  11705  resqrexlemdecn  11722  resqrexlemcalc3  11726  resqrexlemcvg  11729  resqrexlemoverl  11731  leabs  11784  absexpzap  11790  ltabs  11797  abslt  11798  absle  11799  maxleim  11915  maxabslemval  11918  fimaxre2  11937  minmax  11940  2zinfmin  11953  xrmaxiflemcl  11955  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  xrmaxltsup  11968  xrmaxadd  11971  xrminmax  11975  xrbdtri  11986  2clim  12011  climshftlemg  12012  climsqz  12045  climsqz2  12046  climrecvg1n  12058  climcvg1nlem  12059  serf0  12062  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  summodclem2  12093  zsumdc  12095  fsum3  12098  isumss  12102  fisumss  12103  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fsumsplit  12118  sumsnf  12120  fsum2d  12146  fisum0diag2  12158  fsummulc2  12159  modfsummod  12169  fsumabs  12176  fsumrelem  12182  fsumiun  12188  geoisumr  12229  cvgratnnlemseq  12237  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  fprodssdc  12301  fprodmul  12302  prodsnf  12303  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcl2lem  12316  fprodap0  12332  fprod2d  12334  fprodrec  12340  fprodap0f  12347  efcj  12384  efaddlem  12385  tanaddaplem  12449  sinltxirr  12472  nndivides  12508  dvdsext  12566  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  bitsfzolem  12665  bitsmod  12667  bitsinv1  12673  dvdsbnd  12677  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlemeu  12728  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  dfgcd2  12735  bezoutr1  12754  nnmindc  12755  nninfctlemfo  12761  dvdslcm  12791  lcmgcdlem  12799  qredeq  12818  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  isprm2lem  12838  prmind2  12842  exprmfct  12860  prmdvdsfz  12861  isprm5lem  12863  prmexpb  12873  rpexp1i  12876  sqrt2irr  12884  sqne2sq  12899  nonsq  12929  phiprmpw  12944  eulerthlemrprm  12951  eulerthlema  12952  hashgcdeq  12962  phisum  12963  modprmn0modprm0  12979  pclemub  13010  pclemdc  13011  pcmul  13024  pcqmul  13026  pcxqcl  13035  pcdvdstr  13050  pcprmpw2  13056  difsqpwdvds  13061  pcmpt  13066  oddprmdvds  13077  prmpwdvds  13078  pockthg  13080  infpnlem1  13082  1arith  13090  4sqlem2  13112  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqlem11  13124  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemscl  13191  ballotfilemimin  13193  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsv  13197  ballotfilemsdom  13199  ballotfilemsima  13203  ennnfonelemg  13238  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemfun  13252  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemdm  13255  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinf  13265  ctiunctlemudc  13272  nninfdclemlt  13286  nninfdclemf1  13287  isstruct2r  13307  imasival  13570  gsumpropd2  13656  sgrppropd  13676  mndpropd  13701  issubmnd  13703  mndissubm  13730  resmhm2b  13744  mhmeql  13747  gsumfzz  13750  gsumwsubmcl  13751  gsumwmhm  13753  gsumfzcl  13754  grpinvnz  13826  mhmmnd  13869  mulgfng  13877  mulgz  13903  mulgnndir  13904  mulgnn0dir  13905  mulgneg2  13909  mulgass  13912  mhmmulg  13916  issubgrpd2  13943  issubg4m  13946  grpissubg  13947  isnsg3  13960  ghmpreima  14019  ghmnsgpreima  14022  ghmf1  14026  conjnmz  14032  conjnmzb  14033  eqgabl  14083  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gfsumval  14102  gfsumcl  14110  prdsval  14115  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  pws0g  14155  pwssub  14158  rngpropd  14194  issrg  14208  ringpropd  14281  ringinvnz1ne0  14292  dvdsrvald  14338  dvdsrd  14339  dvdsrtr  14346  unitgrp  14361  rhmopp  14421  aprnzr  14537  opprdrng  14558  lmodfopne  14600  lmodprop2d  14622  lssvacl  14639  lsslss  14655  lss1d  14657  lsspropdg  14705  rnglidlmcl  14754  lidlacl  14758  isridl  14778  znidomb  14932  znunit  14933  znrrg  14934  psrval  14940  mplsubgfilemcl  14980  mplsubgfileminv  14981  mplsubgfi  14982  tgdom  15063  neipsm  15145  tgrest  15160  cnfval  15185  cnpfval  15186  cnpval  15189  iscnp4  15209  cnpnei  15210  cnptopco  15213  cncnpi  15219  cncnp  15221  cnptopresti  15229  cnptoprest2  15231  cndis  15232  lmtopcnp  15241  txbasval  15258  neitx  15259  txcnp  15262  txcnmpt  15264  txcn  15266  imasnopn  15290  psmetres2  15324  isxmet2d  15339  xblss2ps  15395  xblss2  15396  blbas  15424  neibl  15482  metss2lem  15488  metrest  15497  xmettx  15501  metcnp3  15502  metcnp  15503  metcnp2  15504  metcnpi  15506  metcnpi2  15507  mulc1cncf  15580  cncfco  15582  mulcncflem  15598  mulcncf  15599  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeu  15614  suplociccreex  15615  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicclemicc  15623  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthinc  15634  limcimolemlt  15655  limccnp2lem  15667  limccnp2cntop  15668  limccoap  15669  dvcj  15700  dvmptfsum  15716  dveflem  15717  plyf  15728  plyaddlem1  15738  plymullem1  15739  plycolemc  15749  plyco  15750  plycj  15752  dvply1  15756  dvply2g  15757  efltlemlt  15765  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  coseq0negpitopi  15827  abssinper  15837  cos02pilt1  15842  relogeftb  15856  logbgcd1irraplemexp  15959  logbgcd1irrap  15961  dvdsppwf1o  15983  mpodvdsmulf1o  15984  mersenne  15991  perfectlem2  15994  perfect  15995  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgsval2lem  16009  lgsmod  16025  lgsdilem  16026  lgsdir2lem4  16030  lgsdir2  16032  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  2lgslem1a1  16085  2lgslem1a  16087  2sqlem5  16118  2sqlem6  16119  2sqlem7  16120  2sqlem9  16123  2sqlem10  16124  umgrnloopv  16235  uhgr2edg  16327  upgredginwlk  16477  clwwlkccatlem  16521  eupth2lem3lem3fi  16591  eupth2lem3lem4fi  16594  eupth2lemsfi  16599  depindlem3  16629  bj-findis  16875  pwle2  16898  pwf1oexmid  16899  pw1nct  16903  nnsf  16909  peano4nninf  16910  nninfall  16913  nninfsellemeq  16918  nninfsellemeqinf  16920  nnnninfex  16926  nninfnfiinf  16927  qdencn  16933  refeq  16934  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  trimul0or  16971  nconstwlpolemgt0  16976  nconstwlpolem  16977  neapmkvlem  16979