Theorem ad3antrrr 726

Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antrrr	⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 479	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 722	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  ad4antr  728  ad4antlr  729  ad5ant12  752  simplll  771  fsnex  7283  fimaproj  8123  frxp3  8139  oaabs  8649  oaabs2  8650  omabs  8652  cofon1  8673  undomOLD  9062  sbthlem8  9092  findcard3OLD  9288  cantnfle  9668  cantnfp1  9678  cantnflem1c  9684  sornom  10274  enfin2i  10318  ttukeylem6  10511  fpwwe2lem12  10639  winalim2  10693  wuncval2  10744  negf1o  11648  xlemul1a  13271  difreicc  13465  flflp1  13776  faclbnd  14254  swrdswrd  14659  pfxccatin12lem3  14686  swrdccat3blem  14693  ello12  15464  elo12  15475  rlimclim1  15493  rlimcld2  15526  o1co  15534  o1of2  15561  o1rlimmul  15567  rlimsqzlem  15599  isercoll  15618  o1fsum  15763  supcvg  15806  dvds2ln  16236  lcmgcdlem  16547  cncongr2  16609  isprm5  16648  prmdvdsncoprmbd  16667  pcadd  16826  vdwlem2  16919  vdwlem11  16928  sbcie3s  17099  prdsval  17405  mreexexlem4d  17595  isacs2  17601  catcocl  17633  catass  17634  subccocl  17799  fullsubc  17804  funcco  17825  fullpropd  17875  ffthiso  17884  isnat  17902  natpropd  17933  fucpropd  17934  xpcval  18133  evlf2  18175  curfpropd  18190  curfuncf  18195  uncfcurf  18196  hofcl  18216  hofpropd  18224  yonffthlem  18239  isacs3lem  18499  acsfiindd  18510  gsumpropd2lem  18604  resmgmhm2b  18638  resmhm2b  18739  mhmid  18982  mhmmnd  18983  ghmgrp  18985  conjnmzb  19167  pgpfi  19514  sylow3lem2  19537  efgredlem  19656  frgpnabllem1  19782  imasabl  19785  dprdfcntz  19926  ablfac1b  19981  pgpfac1lem3  19988  pgpfac1lem5  19990  pgpfaclem3  19994  ringinvnzdiv  20189  imadrhmcl  20556  cntzsdrg  20561  islmhm2  20793  lspsneleq  20873  znunit  21338  psgndiflemB  21372  uvcff  21565  uvcf1  21566  lindfmm  21601  sraassab  21641  psrval  21687  psrass1  21744  resspsrmul  21756  mplbas2  21816  mhpmulcl  21911  coe1tmmul  22019  gsummoncoe1  22048  dmatsubcl  22220  scmatscm  22235  smatvscl  22246  marrepval  22284  mdetdiaglem  22320  mdetunilem8  22341  mdetunilem9  22342  pmatcoe1fsupp  22423  decpmatmulsumfsupp  22495  pmatcollpw2lem  22499  mp2pm2mplem4  22531  pm2mpmhmlem1  22540  pm2mpmhmlem2  22541  pm2mp  22547  fvmptnn04if  22571  cpmadugsumfi  22599  cpmidg2sum  22602  cpmadumatpoly  22605  cayhamlem4  22610  neiptoptop  22855  neitr  22904  ordtrest2lem  22927  cnpnei  22988  iscncl  22993  cncls  22998  cnntr  22999  cncnp  23004  lmcnp  23028  isreg2  23101  hauscmplem  23130  cmpfi  23132  1stcfb  23169  1stcrest  23177  2ndcctbss  23179  2ndcomap  23182  islly2  23208  cldllycmp  23219  lly1stc  23220  locfincmp  23250  llycmpkgen2  23274  1stckgenlem  23277  kgencn2  23281  kgencn3  23282  ptbasfi  23305  ptpjopn  23336  txdis1cn  23359  txlly  23360  txnlly  23361  txtube  23364  txcmplem2  23366  tx1stc  23374  txkgen  23376  xkopt  23379  xkoco2cn  23382  xkococnlem  23383  xkococn  23384  xkoinjcn  23411  tgqtop  23436  regr1lem  23463  kqreglem1  23465  nrmhmph  23518  rnelfmlem  23676  rnelfm  23677  fmfnfmlem4  23681  fmfnfm  23682  ufldom  23686  flimopn  23699  hauspwpwf1  23711  fclsopn  23738  fclsnei  23743  fclsrest  23748  alexsublem  23768  alexsubALTlem3  23773  ptcmplem2  23777  ptcmplem3  23778  cnextfun  23788  cnextcn  23791  symgtgp  23830  tgpt0  23843  qustgpopn  23844  tsmsxplem1  23877  trust  23954  utopsnneiplem  23972  utop3cls  23976  utopreg  23977  isucn2  24004  cstucnd  24009  ucncn  24010  fmucnd  24017  cfilufg  24018  neipcfilu  24021  met2ndci  24251  prdsxmslem2  24258  metustid  24283  metustexhalf  24285  metust  24287  psmetutop  24296  nmoleub  24468  reconnlem2  24563  xrge0tsms  24570  cncfco  24647  lebnumlem3  24709  lebnum  24710  nmoleub2lem2  24863  nmoleub3  24866  iscfil2  25014  iscau4  25027  iscmet3lem2  25040  equivcfil  25047  equivcau  25048  caubl  25056  rrxdstprj1  25157  ovolshftlem2  25259  ovolicc2lem4  25269  uniioombl  25338  i1fmulclem  25452  mbfi1fseqlem6  25470  itg2const2  25491  itg2split  25499  bddiblnc  25591  ellimc2  25626  ellimc3  25628  limcflf  25630  dvmptfsum  25727  dvferm1  25737  dvferm2  25739  dvlip2  25747  c1lip1  25749  lhop1  25766  ftc1a  25789  ply1divex  25889  plyeq0lem  25959  plymullem1  25963  coemullem  25999  coemulc  26004  ulmshftlem  26137  ulmcaulem  26142  ulmbdd  26146  ulmcn  26147  ulmdvlem3  26150  mtestbdd  26153  pserulm  26170  pserdvlem2  26176  abelthlem8  26187  xrlimcnp  26709  jensen  26729  lgamucov  26778  logfac2  26956  dchrelbas3  26977  dchrpt  27006  gausslemma2dlem1a  27104  lgsquad3  27126  2sqb  27171  rpvmasumlem  27226  dchrisumlem1  27228  dchrisumlem3  27230  dchrmusum2  27233  dchrvmasumlem2  27237  dchrisum0flblem1  27247  dchrisum0lem1b  27254  dchrisum0lem1  27255  dchrisum0  27259  mulog2sumlem2  27274  pntlem3  27348  ostth3  27377  slerec  27557  cofcutr  27649  istrkgcb  27974  tgbtwndiff  28024  iscgrglt  28032  tgcgrxfr  28036  motcgrg  28062  lnext  28085  tgbtwnconn1  28093  tgbtwnconn3  28095  legval  28102  legtrid  28109  legso  28117  hlcgreu  28136  tglnne  28146  tglineeltr  28149  tglnne0  28158  colline  28167  tglowdim2l  28168  tglowdim2ln  28169  mirreu3  28172  mirbtwnhl  28198  krippenlem  28208  midexlem  28210  perpcom  28231  footexALT  28236  footex  28239  colperpexlem3  28250  colperpex  28251  opphllem  28253  midex  28255  oppne3  28261  opptgdim2  28263  oppnid  28264  opphllem2  28266  opphllem5  28269  opphllem6  28270  oppperpex  28271  outpasch  28273  hlpasch  28274  lnopp2hpgb  28281  hpgerlem  28283  colopp  28287  colhp  28288  lmieu  28302  lnperpex  28321  trgcopy  28322  trgcopyeulem  28323  iscgra1  28328  cgrane1  28330  cgrane2  28331  cgrane3  28332  cgrane4  28333  cgrahl1  28334  cgrahl2  28335  cgracgr  28336  cgraswap  28338  cgracom  28340  cgratr  28341  flatcgra  28342  cgrabtwn  28344  cgrahl  28345  sacgr  28349  acopyeu  28352  cgrg3col4  28371  tgasa1  28376  f1otrg  28389  f1otrge  28390  axeuclidlem  28487  axcontlem2  28490  umgrvad2edg  28737  usgredg2vlem2  28750  pthdepisspth  29259  clwwlkccatlem  29509  clwlkclwwlklem2  29520  3cycld  29698  eupth2lems  29758  eucrctshift  29763  frgr3vlem2  29794  n4cyclfrgr  29811  numclwwlk1lem2f1  29877  numclwwlk2lem1  29896  ubthlem3  30392  chirredlem1  31910  chirredlem3  31912  cdj1i  31953  fnpreimac  32163  xrge0infss  32240  nn0xmulclb  32251  hashxpe  32286  ccatf1  32382  swrdf1  32387  dfmgc2lem  32432  mgcf1o  32440  gsumhashmul  32478  xrge0tsmsd  32479  omndmul2  32500  gsumle  32512  psgnfzto1stlem  32529  cycpmco2  32562  cycpmrn  32572  tocyccntz  32573  cycpmconjslem2  32584  cyc3conja  32586  submarchi  32602  suborng  32703  isarchiofld  32705  imaslmod  32738  znfermltl  32753  lindfpropd  32772  nsgqusf1olem1  32798  ghmquskerlem3  32805  ghmqusker  32806  rhmpreimaidl  32811  unitpidl1  32816  elrspunidl  32820  elrspunsn  32821  rhmimaidl  32824  drngidl  32825  qsidomlem1  32845  mxidlprm  32860  mxidlirredi  32861  qsdrngilem  32882  qsdrngi  32883  evls1fpws  32920  ply1degltdimlem  32995  lindsunlem  32997  lindsun  32998  lbsdiflsp0  32999  dimkerim  33000  fedgmul  33004  extdg1id  33030  evls1fldgencl  33033  minplyirred  33059  smatrcl  33074  1smat1  33082  submateq  33087  mdetpmtr1  33101  madjusmdetlem2  33106  locfinreflem  33118  cmppcmp  33136  rhmpreimacn  33163  ordtrest2NEWlem  33200  ordtconnlem1  33202  lmdvg  33231  esumpcvgval  33374  esum2d  33389  sigapildsys  33458  ldgenpisyslem1  33459  fiunelros  33470  volmeas  33527  imambfm  33559  omssubadd  33597  carsggect  33615  carsgclctunlem3  33617  sgnmul  33839  signsply0  33860  signstres  33884  actfunsnf1o  33914  actfunsnrndisj  33915  reprsuc  33925  reprinfz1  33932  breprexplema  33940  breprexplemc  33942  breprexp  33943  breprexpnat  33944  circlemeth  33950  hgt750lemb  33966  tgoldbachgtd  33972  erdszelem8  34487  pconnconn  34520  cvmlift2lem12  34603  cvmlift3lem5  34612  cvmlift3lem7  34614  cvmlift3lem8  34615  mrsubrn  34802  msrval  34827  msubff1  34845  btwnconn1lem13  35375  elicc3  35505  neibastop2lem  35548  unbdqndv2  35690  irrdifflemf  36509  ltflcei  36779  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem4  36795  poimirlem13  36804  poimirlem14  36805  poimirlem22  36813  poimirlem26  36817  poimirlem27  36818  heicant  36826  mblfinlem2  36829  mblfinlem3  36830  mblfinlem4  36831  cnambfre  36839  itg2addnclem  36842  itg2addnclem2  36843  itg2gt0cn  36846  ftc1cnnc  36863  ftc1anclem5  36868  ftc1anclem7  36870  ftc1anc  36872  equivtotbnd  36949  isbndx  36953  ssbnd  36959  heibor1lem  36980  rrncmslem  37003  islshpat  38190  lfl1dim  38294  lfl1dim2N  38295  lkrpssN  38336  glbconN  38550  glbconNOLD  38551  hlhgt2  38563  3dim2  38642  3dim3  38643  islln3  38684  islvol5  38753  2lplnja  38793  dalem19  38856  isline4N  38951  2polssN  39089  lhpmatb  39205  4atex  39250  trlatn0  39346  cdlemf2  39736  dialss  40220  diaglbN  40229  diaintclN  40232  dibglbN  40340  dibintclN  40341  dihlsscpre  40408  dihglblem5aN  40466  dihglblem2aN  40467  dihglblem4  40471  dihatexv  40512  dihjat1lem  40602  lcfl6  40674  mapdval2N  40804  aks4d1p8  41258  fldhmf1  41261  sticksstones8  41275  sticksstones12a  41279  imacrhmcl  41393  evlsvvval  41437  evlselv  41461  fsuppind  41464  sn-0tie0  41614  prjspertr  41649  prjspreln0  41653  prjspner1  41670  elrfi  41734  eldioph2  41802  diophin  41812  irrapxlem2  41863  irrapxlem3  41864  irrapxlem4  41865  irrapxlem5  41866  pell1234qrne0  41893  pell1234qrreccl  41894  pell1234qrmulcl  41895  pell14qrgt0  41899  pell14qrdich  41909  pell1qrge1  41910  pellfundex  41926  congabseq  42015  jm2.27b  42047  jm2.27  42049  fnwe2lem2  42095  kelac1  42107  lnrfg  42163  hbt  42174  nadd1suc  42444  rfovcnvf1od  43057  ntrneiiso  43144  ntrneikb  43147  ntrneixb  43148  ntrneik3  43149  ntrneix3  43150  ntrneik13  43151  ntrneix13  43152  cvgdvgrat  43374  binomcxplemnotnn0  43417  sineq0ALT  44000  disjf1  44180  supxrgere  44341  supxrgelem  44345  supxrge  44346  suplesup  44347  xralrple2  44362  infxr  44375  infleinflem2  44379  infleinf  44380  uzub  44439  mccl  44612  limcrecl  44643  lptioo2  44645  lptioo1  44646  lptre2pt  44654  addlimc  44662  limsupmnflem  44734  climxrre  44764  liminflimsupclim  44821  climxlim2lem  44859  xlimliminflimsup  44876  icccncfext  44901  cncfiooicclem1  44907  cncfiooiccre  44909  dvbdfbdioolem2  44943  ioodvbdlimc1lem1  44945  dvnxpaek  44956  dvmptfprodlem  44958  dvmptfprod  44959  dvnprodlem3  44962  itgioocnicc  44991  itgspltprt  44993  stoweidlem31  45045  fourierdlem39  45160  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem51  45171  fourierdlem64  45184  fourierdlem65  45185  fourierdlem74  45194  fourierdlem75  45195  fourierdlem81  45201  fourierdlem82  45202  fourierdlem101  45221  etransclem23  45271  etransclem27  45275  etransclem32  45280  etransclem33  45281  etransclem35  45283  etransclem38  45286  sge0tsms  45394  sge0cl  45395  sge0f1o  45396  sge0split  45423  sge0rpcpnf  45435  sge0seq  45460  nnfoctbdjlem  45469  iundjiun  45474  meaiuninc3v  45498  meaiininclem  45500  omeiunltfirp  45533  carageniuncllem2  45536  carageniuncl  45537  hoidmv1lelem1  45605  hoidmvlelem3  45611  hoidmvlelem5  45613  hoidmvle  45614  hoiqssbllem3  45638  iunhoiioolem  45689  pimdecfgtioo  45731  pimincfltioo  45732  preimageiingt  45734  preimaleiinlt  45735  smflimlem4  45788  iccpartigtl  46389  iccpartgt  46393  sprsymrelf1lem  46457  paireqne  46477  proththd  46580  requad2  46589  sbgoldbst  46744  bgoldbtbndlem4  46774  isomushgr  46792  isomuspgrlem2d  46797  2zrngmmgm  46932  cznrng  46941  rnghmsubcsetclem2  46962  rhmsubcsetclem2  47008  srhmsubc  47062  rhmsubclem4  47075  srhmsubcALTV  47080  rhmsubcALTVlem4  47093  lincsum  47197  lcoss  47204  snlindsntor  47239  islindeps2  47251  line2x  47527  line2y  47528  itscnhlinecirc02p  47558