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  7319  ordiso2  7376  updjud  7423  difinfsnlem  7440  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  enumct  7456  nnnninfeq  7469  nninfisol  7474  enomnilem  7479  fodju0  7488  enmkvlem  7502  enwomnilem  7510  nninfwlpoimlemg  7516  pr1or2  7541  pr2cv1  7542  exmidfodomrlemim  7554  exmidontriimlem2  7579  exmidapne  7627  cc3  7635  dfplpq2  7722  nqpi  7746  nqnq0pi  7806  nq0nn  7810  elinp  7842  elnp1st2nd  7844  genprndl  7889  genprndu  7890  addnqprllem  7895  addnqprulem  7896  addnqprl  7897  addnqpru  7898  addlocpr  7904  nqprloc  7913  prmuloc  7934  mulnqprl  7936  mulnqpru  7937  mullocpr  7939  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  archrecpr  8032  caucvgprlemnkj  8034  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnjltk  8059  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemdisj  8070  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  caucvgprprlemaddq  8076  suplocexprlemru  8087  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  suplocexprlemlub  8092  mulgt0sr  8146  caucvgsrlemcau  8161  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axsuploc  8399  cnegexlem1  8503  cnegex  8506  apsym  8937  apcotr  8938  apadd1  8939  mulext1  8943  mulge0  8950  apti  8953  aprcl  8977  conjmulap  9062  lemulge11  9199  creui  9293  nndiv  9348  zaddcllemneg  9688  suprzclex  9749  eluzuzle  9940  infregelbex  10008  divfnzn  10031  qapne  10049  xrltso  10209  xnn0dcle  10215  xnn0letri  10216  xrre  10233  xrre3  10235  xaddf  10257  xaddval  10258  xpncan  10284  xleadd1a  10286  xltadd1  10289  xleaddadd  10300  ixxss12  10319  elioc2  10349  elico2  10350  elicc2  10351  fzm1  10518  fzneuz  10519  eluzgtdifelfzo  10626  elfzonelfzo  10659  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  flaplt  10733  modqid  10801  modqcyc2  10812  modqmuladd  10818  modqmuladdnn0  10820  modaddmodlo  10840  addmodlteq  10850  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgsuc  10866  frecuzrdgsuctlem  10875  nninfinf  10895  seq3clss  10923  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemmo  10957  iseqf1olemqf1o  10958  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1olemp  10967  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem1  10971  seqf1oglem2  10972  seqf1og  10973  seq3id3  10976  seqfeq4g  10983  ser3ge0  10988  exp3val  10993  expap0  11021  qsqeqor  11102  modqexp  11119  nn0sqdc  11162  nn0ltexp2  11163  facndiv  11193  faclbnd  11195  bcval5  11217  hashunlem  11260  hashun  11261  hashprg  11265  fiprsshashgt1  11274  hashfacen  11300  hashf1lem1  11301  zfz1isolemiso  11307  zfz1isolem1  11308  seq3coll  11310  hashtpglem  11314  ccatcl  11377  ccatlen  11379  ccatvalfn  11385  ccatsymb  11386  ccatrn  11393  ccat2s1fstg  11432  swrdclg  11438  swrdspsleq  11455  pfxeq  11484  swrdswrd  11493  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12  11521  pfxccat3  11522  swrdccat3b  11528  reuccatpfxs1  11535  ovshftex  11600  2shfti  11612  seq3shft  11619  cjap  11688  caucvgrelemcau  11762  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniq  11777  resqrexlemdecn  11794  resqrexlemcalc3  11798  resqrexlemcvg  11801  resqrexlemoverl  11803  leabs  11856  absexpzap  11863  ltabs  11870  abslt  11871  absle  11872  maxleim  11988  maxabslemval  11991  fimaxre2  12010  fiidxsupcl  12012  minmax  12014  2zinfmin  12028  xrmaxiflemcl  12030  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  xrmaxltsup  12043  xrmaxadd  12046  xrminmax  12050  xrbdtri  12061  2clim  12086  climshftlemg  12087  climsqz  12120  climsqz2  12121  climrecvg1n  12133  climcvg1nlem  12134  serf0  12137  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  summodclem2  12168  zsumdc  12170  fsum3  12173  isumss  12177  fisumss  12178  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  fsumsplit  12193  sumsnf  12195  fsum2d  12221  fisum0diag2  12233  fsummulc2  12234  modfsummod  12244  fsumabs  12251  fsumrelem  12257  fsumiun  12263  geoisumr  12304  cvgratnnlemseq  12312  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodntrivap  12370  fprodssdc  12376  fprodmul  12377  prodsnf  12378  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  fprodcl2lem  12391  fprodap0  12407  fprod2d  12409  fprodrec  12415  fprodap0f  12422  efcj  12459  efaddlem  12460  tanaddaplem  12524  sinltxirr  12547  nndivides  12583  dvdsext  12641  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  bitsfzolem  12740  bitsmod  12742  bitsinv1  12748  dvdsbnd  12752  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemzz  12798  bezoutlemaz  12799  bezoutlembz  12800  bezoutlemeu  12803  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  dfgcd2  12810  bezoutr1  12829  nnmindc  12830  nninfctlemfo  12836  dvdslcm  12866  lcmgcdlem  12874  qredeq  12893  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  isprm2lem  12913  prmind2  12917  exprmfct  12936  prmdvdsfz  12937  isprm5lem  12939  prmexpb  12949  rpexp1i  12952  sqrt2irr  12960  pwbdvdslemn  12963  sqne2sq  12976  nonsq  13006  phiprmpw  13023  eulerthlemrprm  13030  eulerthlema  13031  hashgcdeq  13041  phisum  13042  modprmn0modprm0  13058  pclemub  13089  pclemdc  13090  pcmul  13103  pcqmul  13105  pcxqcl  13114  pcdvdstr  13129  pcprmpw2  13135  difsqpwdvds  13140  pcmpt  13145  oddprmdvds  13156  prmpwdvds  13157  pockthg  13159  infpnlem1  13161  1arith  13169  4sqlem2  13191  4sqlemafi  13197  4sqlemffi  13198  4sqleminfi  13199  4sqlem11  13203  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemscl  13299  ballotfilemimin  13301  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsv  13305  ballotfilemsdom  13307  ballotfilemsima  13311  ennnfonelemg  13346  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemfun  13360  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemdm  13363  ennnfonelemnn0  13365  ennnfonelemim  13367  exmidunben  13369  ctinfomlemom  13370  ctinf  13373  ctiunctlemudc  13380  nninfdclemlt  13394  nninfdclemf1  13395  isstruct2r  13415  imasival  13680  sgrppropd  13781  mndpropd  13806  issubmnd  13808  mndissubm  13835  resmhm2b  13849  mhmeql  13852  gzsumwsubmcl  13854  gzsumwmhm  13856  gzsumcl  13857  grpinvnz  13929  mhmmnd  13972  mulgfng  13980  mulgz  14006  mulgnndir  14007  mulgnn0dir  14008  mulgneg2  14012  mulgass  14015  mhmmulg  14019  issubgrpd2  14046  issubg4m  14049  grpissubg  14050  isnsg3  14063  ghmpreima  14122  ghmnsgpreima  14125  ghmf1  14129  conjnmz  14135  conjnmzb  14136  cntrsubgnsg  14169  eqgabl  14218  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gsumvalfi  14236  gsumclfi  14243  gsumf1ofi  14244  gsummptfidmadd  14245  gsumsubmclfi  14247  prdsval  14257  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  pws0g  14297  pwssub  14300  rngpropd  14338  issrg  14353  ringpropd  14427  ringinvnz1ne0  14438  dvdsrvald  14484  dvdsrd  14485  dvdsrtr  14492  unitgrp  14507  rhmopp  14567  aprnzr  14683  opprdrng  14704  lmodfopne  14747  lmodprop2d  14769  lssvacl  14786  lsslss  14802  lss1d  14804  lsspropdg  14852  rnglidlmcl  14901  lidlacl  14905  isridl  14925  gsumfsum  15007  znidomb  15077  znunit  15078  znrrg  15079  issubassa2  15119  psrval  15134  psrbaglefifi  15147  rhmpsrfilem2  15157  mplsubgfilemcl  15181  mplsubgfileminv  15182  mplsubgfi  15183  tgdom  15264  neipsm  15346  tgrest  15361  cnfval  15386  cnpfval  15387  cnpval  15390  iscnp4  15410  cnpnei  15411  cnptopco  15414  cncnpi  15420  cncnp  15422  cnptopresti  15430  cnptoprest2  15432  cndis  15433  lmtopcnp  15442  txbasval  15459  neitx  15460  txcnp  15463  txcnmpt  15465  txcn  15467  imasnopn  15491  psmetres2  15525  isxmet2d  15540  xblss2ps  15596  xblss2  15597  blbas  15625  neibl  15683  metss2lem  15689  metrest  15698  xmettx  15702  metcnp3  15703  metcnp  15704  metcnp2  15705  metcnpi  15707  metcnpi2  15708  mulc1cncf  15781  cncfco  15783  mulcncflem  15799  mulcncf  15800  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeu  15815  suplociccreex  15816  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemicc  15824  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthinc  15835  limcimolemlt  15856  limccnp2lem  15868  limccnp2cntop  15869  limccoap  15870  dvcj  15901  dvmptfsum  15917  dveflem  15918  plyf  15929  plyaddlem1  15939  plymullem1  15940  plycolemc  15950  plyco  15951  plycj  15953  dvply1  15957  dvply2g  15958  efltlemlt  15966  efap1p  15971  sin0pilem1  15974  sin0pilem2  15975  pilem3  15976  coseq0negpitopi  16029  abssinper  16039  cos02pilt1  16044  relogeftb  16058  logdivlt  16088  logbgcd1irraplemexp  16165  logbgcd1irrap  16167  birthdaylem2  16187  ppiqltx  16242  dvdsppwf1o  16244  mpodvdsmulf1o  16245  ppiqub  16254  chtqub  16257  mersenne  16258  perfectlem2  16261  perfect  16262  pcbcctr  16264  bposlem1  16272  bposlem3  16274  bposlem5  16276  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgsval2lem  16295  lgsmod  16311  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2  16318  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  2lgslem1a1  16371  2lgslem1a  16373  2sqlem5  16404  2sqlem6  16405  2sqlem7  16406  2sqlem9  16409  2sqlem10  16410  umgrnloopv  16521  uhgr2edg  16613  upgredginwlk  16763  clwwlkccatlem  16807  eupth2lem3lem3fi  16877  eupth2lem3lem4fi  16880  eupth2lemsfi  16885  depindlem3  16915  bj-findis  17171  pwle2  17194  pwf1oexmid  17195  pw1nct  17199  wexmiddiffi  17210  nnsf  17214  peano4nninf  17215  nninfall  17218  nninfsellemeq  17223  nninfsellemeqinf  17225  nnnninfex  17231  nninfnfiinf  17232  qdencn  17238  refeq  17239  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  nconstwlpolemgt0  17281  nconstwlpolem  17282  neapmkvlem  17284