Theorem ad3antrrr 729

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 482	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 725	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ad4antr  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7278  fimaproj  8118  frxp3  8134  oaabs  8644  oaabs2  8645  omabs  8647  cofon1  8668  undomOLD  9057  sbthlem8  9087  findcard3OLD  9283  cantnfle  9663  cantnfp1  9673  cantnflem1c  9679  sornom  10269  enfin2i  10313  ttukeylem6  10506  fpwwe2lem12  10634  winalim2  10688  wuncval2  10739  negf1o  11641  xlemul1a  13264  difreicc  13458  flflp1  13769  faclbnd  14247  swrdswrd  14652  pfxccatin12lem3  14679  swrdccat3blem  14686  ello12  15457  elo12  15468  rlimclim1  15486  rlimcld2  15519  o1co  15527  o1of2  15554  o1rlimmul  15560  rlimsqzlem  15592  isercoll  15611  o1fsum  15756  supcvg  15799  dvds2ln  16229  lcmgcdlem  16540  cncongr2  16602  isprm5  16641  prmdvdsncoprmbd  16660  pcadd  16819  vdwlem2  16912  vdwlem11  16921  sbcie3s  17092  prdsval  17398  mreexexlem4d  17588  isacs2  17594  catcocl  17626  catass  17627  subccocl  17792  fullsubc  17797  funcco  17818  fullpropd  17868  ffthiso  17877  isnat  17895  natpropd  17926  fucpropd  17927  xpcval  18126  evlf2  18168  curfpropd  18183  curfuncf  18188  uncfcurf  18189  hofcl  18209  hofpropd  18217  yonffthlem  18232  isacs3lem  18492  acsfiindd  18503  gsumpropd2lem  18595  resmhm2b  18700  mhmid  18941  mhmmnd  18942  ghmgrp  18944  conjnmzb  19122  pgpfi  19468  sylow3lem2  19491  efgredlem  19610  frgpnabllem1  19736  imasabl  19739  dprdfcntz  19880  ablfac1b  19935  pgpfac1lem3  19942  pgpfac1lem5  19944  pgpfaclem3  19948  ringinvnzdiv  20107  imadrhmcl  20406  cntzsdrg  20411  islmhm2  20642  lspsneleq  20721  znunit  21111  psgndiflemB  21145  uvcff  21338  uvcf1  21339  lindfmm  21374  sraassab  21414  psrval  21460  psrass1  21517  resspsrmul  21529  mplbas2  21589  mhpmulcl  21684  coe1tmmul  21791  gsummoncoe1  21820  dmatsubcl  21992  scmatscm  22007  smatvscl  22018  marrepval  22056  mdetdiaglem  22092  mdetunilem8  22113  mdetunilem9  22114  pmatcoe1fsupp  22195  decpmatmulsumfsupp  22267  pmatcollpw2lem  22271  mp2pm2mplem4  22303  pm2mpmhmlem1  22312  pm2mpmhmlem2  22313  pm2mp  22319  fvmptnn04if  22343  cpmadugsumfi  22371  cpmidg2sum  22374  cpmadumatpoly  22377  cayhamlem4  22382  neiptoptop  22627  neitr  22676  ordtrest2lem  22699  cnpnei  22760  iscncl  22765  cncls  22770  cnntr  22771  cncnp  22776  lmcnp  22800  isreg2  22873  hauscmplem  22902  cmpfi  22904  1stcfb  22941  1stcrest  22949  2ndcctbss  22951  2ndcomap  22954  islly2  22980  cldllycmp  22991  lly1stc  22992  locfincmp  23022  llycmpkgen2  23046  1stckgenlem  23049  kgencn2  23053  kgencn3  23054  ptbasfi  23077  ptpjopn  23108  txdis1cn  23131  txlly  23132  txnlly  23133  txtube  23136  txcmplem2  23138  tx1stc  23146  txkgen  23148  xkopt  23151  xkoco2cn  23154  xkococnlem  23155  xkococn  23156  xkoinjcn  23183  tgqtop  23208  regr1lem  23235  kqreglem1  23237  nrmhmph  23290  rnelfmlem  23448  rnelfm  23449  fmfnfmlem4  23453  fmfnfm  23454  ufldom  23458  flimopn  23471  hauspwpwf1  23483  fclsopn  23510  fclsnei  23515  fclsrest  23520  alexsublem  23540  alexsubALTlem3  23545  ptcmplem2  23549  ptcmplem3  23550  cnextfun  23560  cnextcn  23563  symgtgp  23602  tgpt0  23615  qustgpopn  23616  tsmsxplem1  23649  trust  23726  utopsnneiplem  23744  utop3cls  23748  utopreg  23749  isucn2  23776  cstucnd  23781  ucncn  23782  fmucnd  23789  cfilufg  23790  neipcfilu  23793  met2ndci  24023  prdsxmslem2  24030  metustid  24055  metustexhalf  24057  metust  24059  psmetutop  24068  nmoleub  24240  reconnlem2  24335  xrge0tsms  24342  cncfco  24415  lebnumlem3  24471  lebnum  24472  nmoleub2lem2  24624  nmoleub3  24627  iscfil2  24775  iscau4  24788  iscmet3lem2  24801  equivcfil  24808  equivcau  24809  caubl  24817  rrxdstprj1  24918  ovolshftlem2  25019  ovolicc2lem4  25029  uniioombl  25098  i1fmulclem  25212  mbfi1fseqlem6  25230  itg2const2  25251  itg2split  25259  bddiblnc  25351  ellimc2  25386  ellimc3  25388  limcflf  25390  dvmptfsum  25484  dvferm1  25494  dvferm2  25496  dvlip2  25504  c1lip1  25506  lhop1  25523  ftc1a  25546  ply1divex  25646  plyeq0lem  25716  plymullem1  25720  coemullem  25756  coemulc  25761  ulmshftlem  25893  ulmcaulem  25898  ulmbdd  25902  ulmcn  25903  ulmdvlem3  25906  mtestbdd  25909  pserulm  25926  pserdvlem2  25932  abelthlem8  25943  xrlimcnp  26463  jensen  26483  lgamucov  26532  logfac2  26710  dchrelbas3  26731  dchrpt  26760  gausslemma2dlem1a  26858  lgsquad3  26880  2sqb  26925  rpvmasumlem  26980  dchrisumlem1  26982  dchrisumlem3  26984  dchrmusum2  26987  dchrvmasumlem2  26991  dchrisum0flblem1  27001  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0  27013  mulog2sumlem2  27028  pntlem3  27102  ostth3  27131  slerec  27310  cofcutr  27401  istrkgcb  27697  tgbtwndiff  27747  iscgrglt  27755  tgcgrxfr  27759  motcgrg  27785  lnext  27808  tgbtwnconn1  27816  tgbtwnconn3  27818  legval  27825  legtrid  27832  legso  27840  hlcgreu  27859  tglnne  27869  tglineeltr  27872  tglnne0  27881  colline  27890  tglowdim2l  27891  tglowdim2ln  27892  mirreu3  27895  mirbtwnhl  27921  krippenlem  27931  midexlem  27933  perpcom  27954  footexALT  27959  footex  27962  colperpexlem3  27973  colperpex  27974  opphllem  27976  midex  27978  oppne3  27984  opptgdim2  27986  oppnid  27987  opphllem2  27989  opphllem5  27992  opphllem6  27993  oppperpex  27994  outpasch  27996  hlpasch  27997  lnopp2hpgb  28004  hpgerlem  28006  colopp  28010  colhp  28011  lmieu  28025  lnperpex  28044  trgcopy  28045  trgcopyeulem  28046  iscgra1  28051  cgrane1  28053  cgrane2  28054  cgrane3  28055  cgrane4  28056  cgrahl1  28057  cgrahl2  28058  cgracgr  28059  cgraswap  28061  cgracom  28063  cgratr  28064  flatcgra  28065  cgrabtwn  28067  cgrahl  28068  sacgr  28072  acopyeu  28075  cgrg3col4  28094  tgasa1  28099  f1otrg  28112  f1otrge  28113  axeuclidlem  28210  axcontlem2  28213  umgrvad2edg  28460  usgredg2vlem2  28473  pthdepisspth  28982  clwwlkccatlem  29232  clwlkclwwlklem2  29243  3cycld  29421  eupth2lems  29481  eucrctshift  29486  frgr3vlem2  29517  n4cyclfrgr  29534  numclwwlk1lem2f1  29600  numclwwlk2lem1  29619  ubthlem3  30113  chirredlem1  31631  chirredlem3  31633  cdj1i  31674  fnpreimac  31884  xrge0infss  31961  nn0xmulclb  31972  hashxpe  32007  ccatf1  32103  swrdf1  32108  dfmgc2lem  32153  mgcf1o  32161  gsumhashmul  32196  xrge0tsmsd  32197  omndmul2  32218  gsumle  32230  psgnfzto1stlem  32247  cycpmco2  32280  cycpmrn  32290  tocyccntz  32291  cycpmconjslem2  32302  cyc3conja  32304  submarchi  32320  suborng  32422  isarchiofld  32424  imaslmod  32457  znfermltl  32468  lindfpropd  32487  nsgqusf1olem1  32513  ghmquskerlem3  32520  ghmqusker  32521  rhmpreimaidl  32526  unitpidl1  32531  elrspunidl  32535  elrspunsn  32536  rhmimaidl  32539  drngidl  32540  qsidomlem1  32560  mxidlprm  32575  mxidlirredi  32576  qsdrngilem  32597  qsdrngi  32598  evls1fpws  32635  ply1degltdimlem  32696  lindsunlem  32698  lindsun  32699  lbsdiflsp0  32700  dimkerim  32701  fedgmul  32705  extdg1id  32731  minplyirred  32759  smatrcl  32765  1smat1  32773  submateq  32778  mdetpmtr1  32792  madjusmdetlem2  32797  locfinreflem  32809  cmppcmp  32827  rhmpreimacn  32854  ordtrest2NEWlem  32891  ordtconnlem1  32893  lmdvg  32922  esumpcvgval  33065  esum2d  33080  sigapildsys  33149  ldgenpisyslem1  33150  fiunelros  33161  volmeas  33218  imambfm  33250  omssubadd  33288  carsggect  33306  carsgclctunlem3  33308  sgnmul  33530  signsply0  33551  signstres  33575  actfunsnf1o  33605  actfunsnrndisj  33606  reprsuc  33616  reprinfz1  33623  breprexplema  33631  breprexplemc  33633  breprexp  33634  breprexpnat  33635  circlemeth  33641  hgt750lemb  33657  tgoldbachgtd  33663  erdszelem8  34178  pconnconn  34211  cvmlift2lem12  34294  cvmlift3lem5  34303  cvmlift3lem7  34305  cvmlift3lem8  34306  mrsubrn  34493  msrval  34518  msubff1  34536  btwnconn1lem13  35060  elicc3  35191  neibastop2lem  35234  unbdqndv2  35376  irrdifflemf  36195  ltflcei  36465  lindsenlbs  36472  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem4  36481  poimirlem13  36490  poimirlem14  36491  poimirlem22  36499  poimirlem26  36503  poimirlem27  36504  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  cnambfre  36525  itg2addnclem  36528  itg2addnclem2  36529  itg2gt0cn  36532  ftc1cnnc  36549  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anc  36558  equivtotbnd  36635  isbndx  36639  ssbnd  36645  heibor1lem  36666  rrncmslem  36689  islshpat  37876  lfl1dim  37980  lfl1dim2N  37981  lkrpssN  38022  glbconN  38236  glbconNOLD  38237  hlhgt2  38249  3dim2  38328  3dim3  38329  islln3  38370  islvol5  38439  2lplnja  38479  dalem19  38542  isline4N  38637  2polssN  38775  lhpmatb  38891  4atex  38936  trlatn0  39032  cdlemf2  39422  dialss  39906  diaglbN  39915  diaintclN  39918  dibglbN  40026  dibintclN  40027  dihlsscpre  40094  dihglblem5aN  40152  dihglblem2aN  40153  dihglblem4  40157  dihatexv  40198  dihjat1lem  40288  lcfl6  40360  mapdval2N  40490  aks4d1p8  40941  fldhmf1  40944  sticksstones8  40958  sticksstones12a  40962  imacrhmcl  41087  evlsvvval  41133  evlselv  41157  fsuppind  41160  sn-0tie0  41309  prjspertr  41344  prjspreln0  41348  prjspner1  41365  elrfi  41418  eldioph2  41486  diophin  41496  irrapxlem2  41547  irrapxlem3  41548  irrapxlem4  41549  irrapxlem5  41550  pell1234qrne0  41577  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell14qrgt0  41583  pell14qrdich  41593  pell1qrge1  41594  pellfundex  41610  congabseq  41699  jm2.27b  41731  jm2.27  41733  fnwe2lem2  41779  kelac1  41791  lnrfg  41847  hbt  41858  nadd1suc  42128  rfovcnvf1od  42741  ntrneiiso  42828  ntrneikb  42831  ntrneixb  42832  ntrneik3  42833  ntrneix3  42834  ntrneik13  42835  ntrneix13  42836  cvgdvgrat  43058  binomcxplemnotnn0  43101  sineq0ALT  43684  disjf1  43866  supxrgere  44030  supxrgelem  44034  supxrge  44035  suplesup  44036  xralrple2  44051  infxr  44064  infleinflem2  44068  infleinf  44069  uzub  44128  mccl  44301  limcrecl  44332  lptioo2  44334  lptioo1  44335  lptre2pt  44343  addlimc  44351  limsupmnflem  44423  climxrre  44453  liminflimsupclim  44510  climxlim2lem  44548  xlimliminflimsup  44565  icccncfext  44590  cncfiooicclem1  44596  cncfiooiccre  44598  dvbdfbdioolem2  44632  ioodvbdlimc1lem1  44634  dvnxpaek  44645  dvmptfprodlem  44647  dvmptfprod  44648  dvnprodlem3  44651  itgioocnicc  44680  itgspltprt  44682  stoweidlem31  44734  fourierdlem39  44849  fourierdlem42  44852  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem51  44860  fourierdlem64  44873  fourierdlem65  44874  fourierdlem74  44883  fourierdlem75  44884  fourierdlem81  44890  fourierdlem82  44891  fourierdlem101  44910  etransclem23  44960  etransclem27  44964  etransclem32  44969  etransclem33  44970  etransclem35  44972  etransclem38  44975  sge0tsms  45083  sge0cl  45084  sge0f1o  45085  sge0split  45112  sge0rpcpnf  45124  sge0seq  45149  nnfoctbdjlem  45158  iundjiun  45163  meaiuninc3v  45187  meaiininclem  45189  omeiunltfirp  45222  carageniuncllem2  45225  carageniuncl  45226  hoidmv1lelem1  45294  hoidmvlelem3  45300  hoidmvlelem5  45302  hoidmvle  45303  hoiqssbllem3  45327  iunhoiioolem  45378  pimdecfgtioo  45420  pimincfltioo  45421  preimageiingt  45423  preimaleiinlt  45424  smflimlem4  45477  iccpartigtl  46078  iccpartgt  46082  sprsymrelf1lem  46146  paireqne  46166  proththd  46269  requad2  46278  sbgoldbst  46433  bgoldbtbndlem4  46463  isomushgr  46481  isomuspgrlem2d  46486  resmgmhm2b  46557  2zrngmmgm  46798  cznrng  46807  rnghmsubcsetclem2  46828  rhmsubcsetclem2  46874  srhmsubc  46928  rhmsubclem4  46941  srhmsubcALTV  46946  rhmsubcALTVlem4  46959  lincsum  47064  lcoss  47071  snlindsntor  47106  islindeps2  47118  line2x  47394  line2y  47395  itscnhlinecirc02p  47425