Theorem ad3antrrr 730

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad4antr  732  ad4antlr  733  simplll  774  fsnex  7258  fimaproj  8114  frxp3  8130  oaabs  8612  oaabs2  8613  omabs  8615  cofon1  8636  sbthlem8  9058  findcard3OLD  9230  cantnfle  9624  cantnfp1  9634  cantnflem1c  9640  sornom  10230  enfin2i  10274  ttukeylem6  10467  fpwwe2lem12  10595  fpwwe2  10596  winalim2  10649  wuncval2  10700  negf1o  11608  xlemul1a  13248  difreicc  13445  flflp1  13769  faclbnd  14255  swrdswrd  14670  swrdccatin1  14690  pfxccatin12lem3  14697  swrdccat3blem  14704  ello12  15482  lo1bdd2  15490  elo12  15493  rlimclim1  15511  rlimcld2  15544  o1co  15552  o1of2  15579  o1rlimmul  15585  rlimsqzlem  15615  isercoll  15634  o1fsum  15779  supcvg  15822  dvds2ln  16259  lcmgcdlem  16576  cncongr2  16638  isprm5  16677  prmdvdsncoprmbd  16697  pcadd  16860  vdwlem2  16953  vdwlem11  16962  sbcie3s  17132  prdsval  17418  mreexexlem4d  17608  isacs2  17614  catcocl  17646  catass  17647  subccocl  17807  fullsubc  17812  funcco  17833  funcpropd  17864  fullpropd  17884  ffthiso  17893  isnat  17912  natpropd  17941  fucpropd  17942  xpcval  18138  evlf2  18179  curfpropd  18194  curfuncf  18199  uncfcurf  18200  curf2ndf  18208  hofcl  18220  hofpropd  18228  yonffthlem  18243  isacs3lem  18501  acsfiindd  18512  gsumpropd2lem  18606  resmgmhm2b  18640  resmhm2b  18749  mhmid  18995  mhmmnd  18996  ghmgrp  18998  conjnmzb  19185  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  pgpfi  19535  sylow3lem2  19558  efgredlem  19677  frgpnabllem1  19803  imasabl  19806  dprdfcntz  19947  ablfac1b  20002  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfaclem3  20015  ringinvnzdiv  20210  rnghmsubcsetclem2  20541  rhmsubcsetclem2  20570  srhmsubc  20589  rhmsubclem4  20597  imadrhmcl  20706  cntzsdrg  20711  islmhm2  20945  lspsneleq  21025  rhmpreimaidl  21187  znunit  21473  psgndiflemB  21509  uvcff  21700  uvcf1  21701  lindfmm  21736  sraassab  21777  psrval  21824  psrass1  21873  resspsrmul  21885  mplbas2  21949  mhpmulcl  22036  psdmul  22053  coe1tmmul  22163  gsummoncoe1  22195  evls1fpws  22256  dmatsubcl  22385  scmatscm  22400  smatvscl  22411  marrepval  22449  mdetdiaglem  22485  mdetunilem8  22506  mdetunilem9  22507  pmatcoe1fsupp  22588  decpmatmulsumfsupp  22660  pmatcollpw2lem  22664  mp2pm2mplem4  22696  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  pm2mp  22712  fvmptnn04if  22736  cpmadugsumfi  22764  cpmidg2sum  22767  cpmadumatpoly  22770  cayhamlem4  22775  neiptoptop  23018  neitr  23067  ordtrest2lem  23090  cnpnei  23151  iscncl  23156  cncls  23161  cnntr  23162  cncnp  23167  lmcnp  23191  isreg2  23264  hauscmplem  23293  cmpfi  23295  1stcfb  23332  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  islly2  23371  cldllycmp  23382  lly1stc  23383  locfincmp  23413  llycmpkgen2  23437  1stckgenlem  23440  kgencn2  23444  kgencn3  23445  ptbasfi  23468  ptpjopn  23499  txdis1cn  23522  txlly  23523  txnlly  23524  txtube  23527  txcmplem2  23529  tx1stc  23537  txkgen  23539  xkopt  23542  xkoco2cn  23545  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  tgqtop  23599  regr1lem  23626  kqreglem1  23628  nrmhmph  23681  rnelfmlem  23839  rnelfm  23840  fmfnfmlem4  23844  fmfnfm  23845  ufldom  23849  flimopn  23862  hauspwpwf1  23874  fclsopn  23901  fclsnei  23906  fclsrest  23911  alexsublem  23931  alexsubALTlem3  23936  ptcmplem2  23940  ptcmplem3  23941  cnextfun  23951  cnextcn  23954  symgtgp  23993  tgpt0  24006  qustgpopn  24007  tsmsxplem1  24040  trust  24117  utopsnneiplem  24135  utop3cls  24139  utopreg  24140  isucn2  24166  cstucnd  24171  ucncn  24172  fmucnd  24179  cfilufg  24180  neipcfilu  24183  met2ndci  24410  prdsxmslem2  24417  metcnp3  24428  metustid  24442  metustexhalf  24444  metust  24446  psmetutop  24455  nmoleub  24619  reconnlem2  24716  xrge0tsms  24723  cncfco  24800  lebnumlem3  24862  lebnum  24863  nmoleub2lem2  25016  nmoleub3  25019  iscfil2  25166  iscau4  25179  iscmet3lem2  25192  equivcfil  25199  equivcau  25200  caubl  25208  rrxdstprj1  25309  ovolshftlem2  25411  ovolicc2lem4  25421  uniioombl  25490  i1fmulclem  25603  mbfi1fseqlem6  25621  itg2const2  25642  itg2split  25650  bddiblnc  25743  ellimc2  25778  ellimc3  25780  limcflf  25782  dvmptfsum  25879  dvferm1  25889  dvferm2  25891  dvlip2  25900  c1lip1  25902  lhop1  25919  ftc1a  25944  ply1divex  26042  plyeq0lem  26115  plymullem1  26119  coemullem  26155  coemulc  26160  ulmshftlem  26298  ulmcaulem  26303  ulmbdd  26307  ulmcn  26308  ulmdvlem3  26311  mtestbdd  26314  pserulm  26331  pserdvlem2  26338  abelthlem8  26349  xrlimcnp  26878  jensen  26899  lgamucov  26948  logfac2  27128  dchrelbas3  27149  dchrpt  27178  gausslemma2dlem1a  27276  lgsquad3  27298  2sqb  27343  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem2  27409  dchrisum0flblem1  27419  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0  27431  mulog2sumlem2  27446  pntlem3  27520  ostth3  27549  slerec  27731  cofcutr  27832  remulscllem2  28352  istrkgcb  28383  tgbtwndiff  28433  iscgrglt  28441  tgcgrxfr  28445  motcgrg  28471  lnext  28494  tgbtwnconn1  28502  tgbtwnconn3  28504  legval  28511  legtrid  28518  legso  28526  hlcgreu  28545  tglnne  28555  tglineeltr  28558  tglnne0  28567  colline  28576  tglowdim2l  28577  tglowdim2ln  28578  mirreu3  28581  mirbtwnhl  28607  krippenlem  28617  midexlem  28619  perpcom  28640  perpneq  28641  footexALT  28645  footex  28648  colperpexlem3  28659  colperpex  28660  opphllem  28662  midex  28664  oppne3  28670  opptgdim2  28672  oppnid  28673  opphllem2  28675  opphllem5  28678  opphllem6  28679  oppperpex  28680  outpasch  28682  hlpasch  28683  lnopp2hpgb  28690  hpgerlem  28692  colopp  28696  colhp  28697  lmieu  28711  lnperpex  28730  trgcopy  28731  trgcopyeulem  28732  iscgra1  28737  cgrane1  28739  cgrane2  28740  cgrane3  28741  cgrane4  28742  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  cgrabtwn  28753  cgrahl  28754  sacgr  28758  acopyeu  28761  cgrg3col4  28780  tgasa1  28785  f1otrg  28798  f1otrge  28799  axeuclidlem  28889  axcontlem2  28892  umgrvad2edg  29140  usgredg2vlem2  29153  pthdepisspth  29665  clwwlkccatlem  29918  clwlkclwwlklem2  29929  3cycld  30107  eupth2lems  30167  eucrctshift  30172  frgr3vlem2  30203  n4cyclfrgr  30220  numclwwlk1lem2f1  30286  numclwwlk2lem1  30305  ubthlem3  30801  chirredlem1  32319  chirredlem3  32321  cdj1i  32362  fnpreimac  32595  xrge0infss  32683  nn0xmulclb  32694  hashxpe  32732  sgnmul  32760  2exple2exp  32770  ccatf1  32870  ccatws1f1o  32873  swrdf1  32878  dfmgc2lem  32921  mgcf1o  32929  chnind  32937  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  gsumfs2d  32995  gsumhashmul  33001  xrge0tsmsd  33002  gsumwun  33005  omndmul2  33026  gsumle  33038  psgnfzto1stlem  33057  cycpmco2  33090  cycpmrn  33100  tocyccntz  33101  cycpmconjslem2  33112  cyc3conja  33114  conjga  33127  submarchi  33140  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  erlval  33209  erler  33216  rloccring  33221  rlocf1  33224  domnprodn0  33226  subrdom  33235  suborng  33293  isarchiofld  33295  imaslmod  33324  znfermltl  33337  lindfpropd  33353  unitprodclb  33360  nsgmgc  33383  nsgqusf1olem1  33384  unitpidl1  33395  elrspunidl  33399  elrspunsn  33400  rhmimaidl  33403  drngidl  33404  qsidomlem1  33423  mxidlprm  33441  mxidlirredi  33442  drngmxidlr  33449  qsdrngilem  33465  qsdrngi  33466  rsprprmprmidl  33493  rsprprmprmidlb  33494  rprmasso2  33497  rprmirred  33502  rprmirredb  33503  rprmdvdspow  33504  1arithidom  33508  pidufd  33514  1arithufdlem3  33517  dfufd2  33521  ply1dg3rt0irred  33551  exsslsb  33592  lbslelsp  33593  ply1degltdimlem  33618  lindsunlem  33620  lindsun  33621  lbsdiflsp0  33622  dimkerim  33623  fedgmul  33627  dimlssid  33628  assalactf1o  33631  extdg1id  33661  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  minplyirred  33701  fldext2chn  33718  cos9thpiminplylem2  33773  smatrcl  33786  1smat1  33794  submateq  33799  mdetpmtr1  33813  madjusmdetlem2  33818  locfinreflem  33830  cmppcmp  33848  rhmpreimacn  33875  ordtrest2NEWlem  33912  ordtconnlem1  33914  lmdvg  33943  zrhcntr  33969  esumpcvgval  34068  esum2d  34083  sigapildsys  34152  ldgenpisyslem1  34153  fiunelros  34164  volmeas  34221  imambfm  34253  omssubadd  34291  carsggect  34309  carsgclctunlem3  34311  signsply0  34542  signstres  34566  actfunsnf1o  34595  actfunsnrndisj  34596  reprsuc  34606  reprinfz1  34613  breprexplema  34621  breprexplemc  34623  breprexp  34624  breprexpnat  34625  circlemeth  34631  hgt750lemb  34647  tgoldbachgtd  34653  erdszelem8  35185  pconnconn  35218  cvmlift2lem12  35301  cvmlift3lem5  35310  cvmlift3lem7  35312  cvmlift3lem8  35313  fmla1  35374  mrsubrn  35500  msrval  35525  msubff1  35543  btwnconn1lem13  36087  elicc3  36305  neibastop2lem  36348  weiunfr  36455  unbdqndv2  36499  irrdifflemf  37313  ltflcei  37602  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem22  37636  poimirlem26  37640  poimirlem27  37641  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  cnambfre  37662  itg2addnclem  37665  itg2addnclem2  37666  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anc  37695  equivtotbnd  37772  isbndx  37776  ssbnd  37782  heibor1lem  37803  rrncmslem  37826  islshpat  39010  lfl1dim  39114  lfl1dim2N  39115  lkrpssN  39156  glbconN  39370  glbconNOLD  39371  hlhgt2  39383  3dim2  39462  3dim3  39463  islln3  39504  islvol5  39573  2lplnja  39613  dalem19  39676  isline4N  39771  2polssN  39909  lhpmatb  40025  4atex  40070  trlatn0  40166  cdlemf2  40556  dialss  41040  diaglbN  41049  diaintclN  41052  dibglbN  41160  dibintclN  41161  dihlsscpre  41228  dihglblem5aN  41286  dihglblem2aN  41287  dihglblem4  41291  dihatexv  41332  dihjat1lem  41422  lcfl6  41494  mapdval2N  41624  aks4d1p8  42075  fldhmf1  42078  primrootscoprmpow  42087  primrootscoprbij2  42091  primrootspoweq0  42094  evl1gprodd  42105  hashscontpow  42110  aks6d1c2lem4  42115  idomnnzgmulnz  42121  deg1gprod  42128  sticksstones8  42141  sticksstones12a  42145  aks6d1c6lem3  42160  aks6d1c6lem5  42165  aks6d1c7  42172  aks5lem5a  42179  unitscyglem2  42184  sn-0tie0  42439  imacrhmcl  42502  fiabv  42524  evlsvvval  42551  evlselv  42575  fsuppind  42578  prjspertr  42593  prjspreln0  42597  prjspner1  42614  elrfi  42682  eldioph2  42750  diophin  42760  irrapxlem2  42811  irrapxlem3  42812  irrapxlem4  42813  irrapxlem5  42814  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrgt0  42847  pell14qrdich  42857  pell1qrge1  42858  pellfundex  42874  congabseq  42963  jm2.27b  42995  jm2.27  42997  fnwe2lem2  43040  kelac1  43052  lnrfg  43108  hbt  43119  omabs2  43321  nadd1suc  43381  rfovcnvf1od  43993  ntrneiiso  44080  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  cvgdvgrat  44302  binomcxplemnotnn0  44345  sineq0ALT  44926  fnchoice  45023  disjf1  45177  supxrgere  45329  supxrgelem  45333  supxrge  45334  suplesup  45335  xralrple2  45350  infxr  45363  infleinflem2  45367  infleinf  45368  uzub  45427  mccl  45596  limcrecl  45627  lptioo2  45629  lptioo1  45630  lptre2pt  45638  addlimc  45646  limsupmnflem  45718  climxrre  45748  liminflimsupclim  45805  climxlim2lem  45843  xlimliminflimsup  45860  icccncfext  45885  cncfiooicclem1  45891  cncfiooiccre  45893  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  dvnxpaek  45940  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem3  45946  itgioocnicc  45975  itgspltprt  45977  stoweidlem31  46029  fourierdlem39  46144  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem81  46185  fourierdlem82  46186  fourierdlem101  46205  etransclem23  46255  etransclem27  46259  etransclem32  46264  etransclem33  46265  etransclem35  46267  etransclem38  46270  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0split  46407  sge0rpcpnf  46419  sge0seq  46444  nnfoctbdjlem  46453  iundjiun  46458  meaiuninc3v  46482  meaiininclem  46484  omeiunltfirp  46517  carageniuncllem2  46520  carageniuncl  46521  hoidmv1lelem1  46589  hoidmvlelem3  46595  hoidmvlelem5  46597  hoidmvle  46598  hoiqssbllem3  46622  iunhoiioolem  46673  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  smflimlem4  46772  iccpartigtl  47424  iccpartgt  47428  sprsymrelf1lem  47492  paireqne  47512  proththd  47615  requad2  47624  sbgoldbst  47779  bgoldbtbndlem4  47809  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrimlem  47895  gricushgr  47917  grimedg  47935  grimgrtri  47948  isubgr3stgrlem7  47971  gpgusgralem  48047  pgn4cyclex  48116  2zrngmmgm  48240  cznrng  48249  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  lincsum  48418  lcoss  48425  snlindsntor  48460  islindeps2  48472  line2x  48743  line2y  48744  itscnhlinecirc02p  48774  discsubc  49053  imasubc3  49145  uppropd  49170  swapfval  49251  fucofvalg  49307  fuco21  49325  precofvalALT  49357  2arwcat  49589  lanup  49630  ranup  49631