Theorem ad3antrrr 743

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4antr  745  ad4antlr  746  simplll  787  fsnex  7292  fimaproj  8140  frxp3  8156  oaabs  8643  oaabs2  8644  omabs  8646  cofon1  8667  sbthlem8  9092  cantnfle  9650  cantnfp1  9660  cantnflem1c  9666  sornom  10279  enfin2i  10323  ttukeylem6  10516  fpwwe2lem12  10645  fpwwe2  10646  winalim2  10699  wuncval2  10750  negf1o  11662  xlemul1a  13332  difreicc  13529  flflp1  13860  faclbnd  14346  ccatf1  14648  swrdf1  14711  swrdswrd  14766  swrdccatin1  14786  pfxccatin12lem3  14793  swrdccat3blem  14800  sgnmul  15170  ello12  15593  lo1bdd2  15601  elo12  15604  rlimclim1  15622  rlimcld2  15655  o1co  15663  o1of2  15690  o1rlimmul  15696  rlimsqzlem  15726  isercoll  15745  o1fsum  15891  supcvg  15936  dvds2ln  16372  lcmgcdlem  16689  cncongr2  16751  isprm5  16791  prmdvdsncoprmbd  16811  pcadd  16974  vdwlem2  17067  vdwlem11  17076  sbcie3s  17247  prdsval  17533  mreexexlem4d  17728  isacs2  17734  catcocl  17766  catass  17767  subccocl  17927  fullsubc  17932  funcco  17953  funcpropd  17984  fullpropd  18004  ffthiso  18013  isnat  18032  natpropd  18061  fucpropd  18062  xpcval  18258  evlf2  18299  curfpropd  18314  curfuncf  18319  uncfcurf  18320  curf2ndf  18328  hofcl  18340  hofpropd  18348  yonffthlem  18363  isacs3lem  18623  acsfiindd  18634  chnind  18702  gsumpropd2lem  18766  resmgmhm2b  18800  resmhm2b  18912  mhmid  19160  mhmmnd  19161  ghmgrp  19163  conjnmzb  19354  ghmqusnsg  19383  ghmquskerlem3  19387  ghmqusker  19388  pgpfi  19706  sylow3lem2  19729  efgredlem  19848  frgpnabllem1  19974  imasabl  19977  dprdfcntz  20118  ablfac1b  20173  pgpfac1lem3  20180  pgpfac1lem5  20182  pgpfaclem3  20186  omndmul2  20234  gsumle  20246  ringinvnzdiv  20417  rnghmsubcsetclem2  20768  rhmsubcsetclem2  20797  srhmsubc  20816  rhmsubclem4  20824  imadrhmcl  20937  cntzsdrg  20942  suborng  21016  islmhm2  21196  lspsneleq  21276  drngidl  21422  rhmpreimaidl  21453  qsidomlem1  21517  prmidlsubm  21524  znunit  21750  psgndiflemB  21787  uvcff  21978  uvcf1  21979  lindfmm  22014  sraassab  22055  psrval  22102  psrass1  22150  resspsrmul  22162  mplbas2  22230  evlsvvval  22281  mhpmulcl  22349  psdmul  22366  coe1tmmul  22475  gsummoncoe1  22505  evls1fpws  22566  dmatsubcl  22692  scmatscm  22707  smatvscl  22718  marrepval  22756  mdetdiaglem  22792  mdetunilem8  22813  mdetunilem9  22814  pmatcoe1fsupp  22895  decpmatmulsumfsupp  22967  pmatcollpw2lem  22971  mp2pm2mplem4  23003  pm2mpmhmlem1  23012  pm2mpmhmlem2  23013  pm2mp  23019  fvmptnn04if  23043  cpmadugsumfi  23071  cpmidg2sum  23074  cpmadumatpoly  23077  cayhamlem4  23082  neiptoptop  23325  neitr  23374  ordtrest2lem  23397  cnpnei  23458  iscncl  23463  cncls  23468  cnntr  23469  cncnp  23474  lmcnp  23498  isreg2  23571  hauscmplem  23600  cmpfi  23602  1stcfb  23639  1stcrest  23647  2ndcctbss  23649  2ndcomap  23652  islly2  23678  cldllycmp  23689  lly1stc  23690  locfincmp  23720  llycmpkgen2  23744  1stckgenlem  23747  kgencn2  23751  kgencn3  23752  ptbasfi  23775  ptpjopn  23806  txdis1cn  23829  txlly  23830  txnlly  23831  txtube  23834  txcmplem2  23836  tx1stc  23844  txkgen  23846  xkopt  23849  xkoco2cn  23852  xkococnlem  23853  xkococn  23854  xkoinjcn  23881  tgqtop  23906  regr1lem  23933  kqreglem1  23935  nrmhmph  23988  rnelfmlem  24146  rnelfm  24147  fmfnfmlem4  24151  fmfnfm  24152  ufldom  24156  flimopn  24169  hauspwpwf1  24181  fclsopn  24208  fclsnei  24213  fclsrest  24218  alexsublem  24238  alexsubALTlem3  24243  ptcmplem2  24247  ptcmplem3  24248  cnextfun  24258  cnextcn  24261  symgtgp  24300  tgpt0  24313  qustgpopn  24314  tsmsxplem1  24347  trust  24423  utopsnneiplem  24441  utop3cls  24445  utopreg  24446  isucn2  24472  cstucnd  24477  ucncn  24478  fmucnd  24485  cfilufg  24486  neipcfilu  24489  met2ndci  24716  prdsxmslem2  24723  metcnp3  24734  metustid  24748  metustexhalf  24750  metust  24752  psmetutop  24761  nmoleub  24925  reconnlem2  25022  xrge0tsms  25029  cncfco  25103  lebnumlem3  25159  lebnum  25160  nmoleub2lem2  25312  nmoleub3  25315  iscfil2  25462  iscau4  25475  iscmet3lem2  25488  equivcfil  25495  equivcau  25496  caubl  25504  rrxdstprj1  25605  ovolshftlem2  25706  ovolicc2lem4  25716  uniioombl  25785  i1fmulclem  25898  mbfi1fseqlem6  25916  itg2const2  25937  itg2split  25945  bddiblnc  26038  ellimc2  26073  ellimc3  26075  limcflf  26077  dvmptfsum  26171  dvferm1  26181  dvferm2  26183  dvlip2  26191  c1lip1  26193  lhop1  26210  ftc1a  26233  ply1divex  26331  plyeq0lem  26404  plymullem1  26408  coemullem  26444  coemulc  26449  ulmshftlem  26589  ulmcaulem  26594  ulmbdd  26598  ulmcn  26599  ulmdvlem3  26602  mtestbdd  26605  pserulm  26622  pserdvlem2  26628  abelthlem8  26639  xrlimcnp  27170  jensen  27190  lgamucov  27239  logfac2  27418  dchrelbas3  27439  dchrpt  27468  gausslemma2dlem1a  27566  lgsquad3  27588  2sqb  27633  rpvmasumlem  27688  dchrisumlem1  27690  dchrisumlem3  27692  dchrmusum2  27695  dchrvmasumlem2  27699  dchrisum0flblem1  27709  dchrisum0lem1b  27716  dchrisum0lem1  27717  dchrisum0  27721  mulog2sumlem2  27736  pntlem3  27810  ostth3  27839  lesrec  28029  cofcutr  28154  remulscllem2  28731  istrkgcb  28762  tgbtwndiff  28812  iscgrglt  28820  tgcgrxfr  28824  motcgrg  28850  lnext  28873  tgbtwnconn1  28881  tgbtwnconn3  28883  legval  28890  legtrid  28897  legso  28905  hlcgreu  28927  tglnne  28938  tglineeltr  28941  tglnne0  28951  colline  28960  tglowdim2l  28961  tglowdim2ln  28962  mirreu3  28968  mirbtwnhl  28994  krippenlem  29004  midexlem  29006  perpcom  29030  perpneq  29031  footexALT  29035  footex  29038  colperpexlem3  29050  colperpex  29051  opphllem  29053  midex  29055  oppne3  29061  opptgdim2  29063  oppnid  29064  opphllem2  29066  opphllem5  29069  opphllem6  29070  oppperpex  29071  outpasch  29074  hlpasch  29075  lnopp2hpgb  29082  hpgerlem  29084  colopp  29088  colhp  29089  plngrnssp  29098  lnincplng  29103  plngrotlem1  29106  plngrotlem2  29107  plngrotlem3  29108  lnssplnglem  29110  lmieu  29130  lnperpex  29150  trgcopy  29152  trgcopyeulem  29153  iscgra1  29158  cgrane1  29160  cgrane2  29161  cgrane3  29162  cgrane4  29163  cgrahl1  29164  cgrahl2  29165  cgracgr  29166  cgraswap  29168  cgracom  29170  cgratr  29171  flatcgra  29172  cgrabtwn  29174  cgrahl  29175  sacgr  29179  acopyeu  29182  ragcgra  29183  cgrg3col4  29207  tgasa1  29212  prlnghpg  29233  dfprlng2  29234  perpprlng  29237  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  prlngplngtr  29246  prlngmid2  29248  quadcgrprlng  29253  f1otrg  29257  f1otrge  29258  axeuclidlem  29349  axcontlem2  29352  umgrvad2edg  29600  usgredg2vlem2  29613  pthdepisspth  30121  clwwlkccatlem  30377  clwlkclwwlklem2  30388  3cycld  30566  eupth2lems  30626  eucrctshift  30631  frgr3vlem2  30662  n4cyclfrgr  30679  numclwwlk1lem2f1  30745  numclwwlk2lem1  30764  ubthlem3  31261  chirredlem1  32779  chirredlem3  32781  cdj1i  32822  fnpreimac  33052  xrge0infss  33142  nn0xmulclb  33153  hashxpe  33189  2exple2exp  33215  ccatws1f1o  33304  dfmgc2lem  33346  mgcf1o  33354  mndlactf1  33377  mndlactfo  33378  mndractf1  33379  mndractfo  33380  gsumfs2d  33412  gsumhashmul  33418  suppgsumssiun  33423  xrge0tsmsd  33424  gsumwun  33427  psgnfzto1stlem  33451  cycpmco2  33484  cycpmrn  33494  tocyccntz  33495  cycpmconjslem2  33506  cyc3conja  33508  conjga  33521  submarchi  33537  isarchiofld  33550  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem3  33595  elrgspnlem4  33596  elrgspnsubrunlem1  33598  elrgspnsubrunlem2  33599  elrgspnsubrun  33600  erlval  33609  erler  33616  rloccring  33622  rlocf1  33625  rlocisunit  33627  domnprodn0  33629  domnprodeq0  33630  subrdom  33636  imaslmod  33704  znfermltl  33712  lindfpropd  33726  unitprodclb  33733  nsgmgc  33752  nsgqusf1olem1  33753  unitpidl1  33763  elrspunidl  33767  elrspunsn  33768  rhmimaidl  33771  mxidlprm  33784  mxidlirredi  33785  drngmxidlr  33791  qsdrngilem  33807  qsdrngi  33808  drnglring  33813  dflringlem2  33816  dflring3  33818  dflring4  33819  rsprprmprmidl  33843  rsprprmprmidlb  33844  rprmasso2  33847  rprmirred  33852  rprmirredb  33853  rprmdvdspow  33854  1arithidom  33858  pidufd  33864  1arithufdlem3  33867  dfufd2  33871  deg1prod  33904  ply1dg3rt0irred  33905  0mplrim  33935  mplidomlem  33948  extvfvcl  33957  mplvrpmga  33966  mplvrpmmhm  33967  mplvrpmrhm  33968  psrgsum  33969  psrmonprod  33973  esplymhp  33989  esplyfval3  33993  esplyfval1  33994  esplyfvaln  33995  esplyind  33996  exsslsb  34018  lbslelsp  34019  ply1degltdimlem  34043  lindsunlem  34045  lindsun  34046  lbsdiflsp0  34047  dimkerim  34048  fedgmul  34052  dimlssid  34053  assalactf1o  34056  extdg1id  34087  evls1fldgencl  34091  fldextrspunlsplem  34094  fldextrspunlsp  34095  extdgfialglem1  34113  minplyirred  34132  fldext2chn  34149  cos9thpiminplylem2  34204  smatrcl  34217  1smat1  34225  submateq  34230  mdetpmtr1  34244  madjusmdetlem2  34249  locfinreflem  34261  cmppcmp  34279  rhmpreimacn  34306  ordtrest2NEWlem  34343  ordtconnlem1  34345  lmdvg  34374  zrhcntr  34400  esumpcvgval  34499  esum2d  34514  sigapildsys  34584  ldgenpisyslem1  34585  fiunelros  34596  volmeas  34653  imambfm  34684  omssubadd  34722  carsggect  34740  carsgclctunlem3  34742  signsply0  34970  signstres  34994  actfunsnf1o  35023  actfunsnrndisj  35024  reprsuc  35034  reprinfz1  35041  breprexplema  35049  breprexplemc  35051  breprexp  35052  breprexpnat  35053  circlemeth  35059  hgt750lemb  35075  tgoldbachgtd  35081  erdszelem8  35711  pconnconn  35744  cvmlift2lem12  35827  cvmlift3lem5  35836  cvmlift3lem7  35838  cvmlift3lem8  35839  fmla1  35900  mrsubrn  36026  msrval  36051  msubff1  36069  btwnconn1lem13  36612  elicc3  36869  neibastop2lem  36912  weiunfr  37019  unbdqndv2  37141  irrdifflemf  38010  ltflcei  38300  lindsenlbs  38307  matunitlindflem1  38308  matunitlindflem2  38309  poimirlem4  38316  poimirlem13  38325  poimirlem14  38326  poimirlem22  38334  poimirlem26  38338  poimirlem27  38339  heicant  38347  mblfinlem2  38350  mblfinlem3  38351  mblfinlem4  38352  cnambfre  38360  itg2addnclem  38363  itg2addnclem2  38364  itg2gt0cn  38367  ftc1cnnc  38384  ftc1anclem5  38389  ftc1anclem7  38391  ftc1anc  38393  equivtotbnd  38470  isbndx  38474  ssbnd  38480  heibor1lem  38501  rrncmslem  38524  islshpat  39832  lfl1dim  39936  lfl1dim2N  39937  lkrpssN  39978  glbconN  40192  hlhgt2  40204  3dim2  40283  3dim3  40284  islln3  40325  islvol5  40394  2lplnja  40434  dalem19  40497  isline4N  40592  2polssN  40730  lhpmatb  40846  4atex  40891  trlatn0  40987  cdlemf2  41377  dialss  41861  diaglbN  41870  diaintclN  41873  dibglbN  41981  dibintclN  41982  dihlsscpre  42049  dihglblem5aN  42107  dihglblem2aN  42108  dihglblem4  42112  dihatexv  42153  dihjat1lem  42243  lcfl6  42315  mapdval2N  42445  aks4d1p8  42895  fldhmf1  42898  primrootscoprmpow  42907  primrootscoprbij2  42911  primrootspoweq0  42914  evl1gprodd  42925  hashscontpow  42930  aks6d1c2lem4  42935  idomnnzgmulnz  42941  deg1gprod  42948  sticksstones8  42961  sticksstones12a  42965  aks6d1c6lem3  42980  aks6d1c6lem5  42985  aks6d1c7  42992  aks5lem5a  42999  unitscyglem2  43004  sn-0tie0  43266  imacrhmcl  43329  fiabv  43345  evlselv  43362  fsuppind  43363  prjspertr  43378  prjspreln0  43382  prjspner1  43399  elrfi  43466  eldioph2  43534  diophin  43544  irrapxlem2  43591  irrapxlem3  43592  irrapxlem4  43593  irrapxlem5  43594  pell1234qrne0  43621  pell1234qrreccl  43622  pell1234qrmulcl  43623  pell14qrgt0  43627  pell14qrdich  43637  pell1qrge1  43638  pellfundex  43654  congabseq  43742  jm2.27b  43774  jm2.27  43776  fnwe2lem2  43819  kelac1  43831  lnrfg  43887  hbt  43898  omabs2  44100  nadd1suc  44160  rfovcnvf1od  44771  ntrneiiso  44858  ntrneikb  44861  ntrneixb  44862  ntrneik3  44863  ntrneix3  44864  ntrneik13  44865  ntrneix13  44866  cvgdvgrat  45064  binomcxplemnotnn0  45107  sineq0ALT  45686  fnchoice  45790  disjf1  45942  supxrgere  46090  supxrgelem  46094  supxrge  46095  suplesup  46096  xralrple2  46111  infxr  46123  infleinflem2  46127  infleinf  46128  uzub  46186  mccl  46355  limcrecl  46386  lptioo2  46388  lptioo1  46389  lptre2pt  46395  addlimc  46403  limsupmnflem  46475  climxrre  46505  liminflimsupclim  46562  climxlim2lem  46600  xlimliminflimsup  46617  icccncfext  46642  cncfiooicclem1  46648  cncfiooiccre  46650  dvbdfbdioolem2  46684  ioodvbdlimc1lem1  46686  dvnxpaek  46697  dvmptfprodlem  46699  dvmptfprod  46700  dvnprodlem3  46703  itgioocnicc  46732  itgspltprt  46734  stoweidlem31  46786  fourierdlem39  46901  fourierdlem42  46904  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem51  46912  fourierdlem64  46925  fourierdlem65  46926  fourierdlem74  46935  fourierdlem75  46936  fourierdlem81  46942  fourierdlem82  46943  fourierdlem101  46962  etransclem23  47012  etransclem27  47016  etransclem32  47021  etransclem33  47022  etransclem35  47024  etransclem38  47027  sge0tsms  47135  sge0cl  47136  sge0f1o  47137  sge0split  47164  sge0rpcpnf  47176  sge0seq  47201  nnfoctbdjlem  47210  iundjiun  47215  meaiuninc3v  47239  meaiininclem  47241  omeiunltfirp  47274  carageniuncllem2  47277  carageniuncl  47278  hoicvr  47303  hoidmv1lelem1  47346  hoidmvlelem3  47352  hoidmvlelem5  47354  hoidmvle  47355  hoiqssbllem3  47379  iunhoiioolem  47430  pimdecfgtioo  47472  pimincfltioo  47473  preimageiingt  47475  preimaleiinlt  47476  smflimlem4  47529  chnerlem1  47639  iccpartigtl  48213  iccpartgt  48217  sprsymrelf1lem  48281  paireqne  48301  proththd  48407  requad2  48429  sbgoldbst  48584  bgoldbtbndlem4  48614  isuspgrim0lem  48699  isuspgrim0  48700  isuspgrimlem  48701  gricushgr  48723  grimedg  48741  grimgrtri  48755  isubgr3stgrlem7  48778  gpgusgralem  48862  pgn4cyclex  48932  2zrngmmgm  49058  cznrng  49067  rhmsubcALTVlem4  49090  srhmsubcALTV  49131  lincsum  49250  lcoss  49257  snlindsntor  49292  islindeps2  49304  line2x  49575  line2y  49576  itscnhlinecirc02p  49606  discsubc  49883  imasubc3  49975  uppropd  50000  swapfval  50081  fucofvalg  50137  fuco21  50155  precofvalALT  50187  2arwcat  50419  lanup  50460  ranup  50461