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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad4antr  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7036  fimaproj  7839  oaabs  8286  oaabs2  8287  omabs  8289  undom  8631  sbthlem8  8661  findcard3  8799  cantnfle  9172  cantnfp1  9182  cantnflem1c  9188  sornom  9742  enfin2i  9786  ttukeylem6  9979  fpwwe2lem12  10107  winalim2  10161  wuncval2  10212  negf1o  11113  xlemul1a  12727  difreicc  12921  flflp1  13231  faclbnd  13705  swrdswrd  14119  pfxccatin12lem3  14146  swrdccat3blem  14153  ello12  14926  elo12  14937  rlimclim1  14955  rlimcld2  14988  o1co  14996  o1of2  15022  o1rlimmul  15028  rlimsqzlem  15058  isercoll  15077  o1fsum  15221  supcvg  15264  dvds2ln  15695  lcmgcdlem  16007  cncongr2  16069  isprm5  16108  prmdvdsncoprmbd  16127  pcadd  16285  vdwlem2  16378  vdwlem11  16387  sbcie3s  16604  prdsval  16791  mreexexlem4d  16981  isacs2  16987  catcocl  17019  catass  17020  subccocl  17179  fullsubc  17184  funcco  17205  fullpropd  17254  ffthiso  17263  isnat  17281  natpropd  17310  fucpropd  17311  xpcval  17498  evlf2  17539  curfpropd  17554  curfuncf  17559  uncfcurf  17560  hofcl  17580  hofpropd  17588  yonffthlem  17603  isacs3lem  17847  acsfiindd  17858  gsumpropd2lem  17960  resmhm2b  18058  mhmid  18292  mhmmnd  18293  ghmgrp  18295  conjnmzb  18465  pgpfi  18802  sylow3lem2  18825  efgredlem  18945  frgpnabllem1  19066  dprdfcntz  19210  ablfac1b  19265  pgpfac1lem3  19272  pgpfac1lem5  19274  pgpfaclem3  19278  ringinvnzdiv  19419  cntzsdrg  19654  islmhm2  19883  lspsneleq  19960  znunit  20336  psgndiflemB  20370  uvcff  20561  uvcf1  20562  lindfmm  20597  psrval  20682  psrass1  20738  resspsrmul  20750  mplbas2  20807  mhpmulcl  20897  coe1tmmul  21006  gsummoncoe1  21033  dmatsubcl  21203  scmatscm  21218  smatvscl  21229  marrepval  21267  mdetdiaglem  21303  mdetunilem8  21324  mdetunilem9  21325  pmatcoe1fsupp  21406  decpmatmulsumfsupp  21478  pmatcollpw2lem  21482  mp2pm2mplem4  21514  pm2mpmhmlem1  21523  pm2mpmhmlem2  21524  pm2mp  21530  fvmptnn04if  21554  cpmadugsumfi  21582  cpmidg2sum  21585  cpmadumatpoly  21588  cayhamlem4  21593  neiptoptop  21836  neitr  21885  ordtrest2lem  21908  cnpnei  21969  iscncl  21974  cncls  21979  cnntr  21980  cncnp  21985  lmcnp  22009  isreg2  22082  hauscmplem  22111  cmpfi  22113  1stcfb  22150  1stcrest  22158  2ndcctbss  22160  2ndcomap  22163  islly2  22189  cldllycmp  22200  lly1stc  22201  locfincmp  22231  llycmpkgen2  22255  1stckgenlem  22258  kgencn2  22262  kgencn3  22263  ptbasfi  22286  ptpjopn  22317  txdis1cn  22340  txlly  22341  txnlly  22342  txtube  22345  txcmplem2  22347  tx1stc  22355  txkgen  22357  xkopt  22360  xkoco2cn  22363  xkococnlem  22364  xkococn  22365  xkoinjcn  22392  tgqtop  22417  regr1lem  22444  kqreglem1  22446  nrmhmph  22499  rnelfmlem  22657  rnelfm  22658  fmfnfmlem4  22662  fmfnfm  22663  ufldom  22667  flimopn  22680  hauspwpwf1  22692  fclsopn  22719  fclsnei  22724  fclsrest  22729  alexsublem  22749  alexsubALTlem3  22754  ptcmplem2  22758  ptcmplem3  22759  cnextfun  22769  cnextcn  22772  symgtgp  22811  tgpt0  22824  qustgpopn  22825  tsmsxplem1  22858  trust  22935  utopsnneiplem  22953  utop3cls  22957  utopreg  22958  isucn2  22985  cstucnd  22990  ucncn  22991  fmucnd  22998  cfilufg  22999  neipcfilu  23002  met2ndci  23229  prdsxmslem2  23236  metustid  23261  metustexhalf  23263  metust  23265  psmetutop  23274  nmoleub  23438  reconnlem2  23533  xrge0tsms  23540  cncfco  23613  lebnumlem3  23669  lebnum  23670  nmoleub2lem2  23822  nmoleub3  23825  iscfil2  23971  iscau4  23984  iscmet3lem2  23997  equivcfil  24004  equivcau  24005  caubl  24013  rrxdstprj1  24114  ovolshftlem2  24215  ovolicc2lem4  24225  uniioombl  24294  i1fmulclem  24407  mbfi1fseqlem6  24425  itg2const2  24446  itg2split  24454  bddiblnc  24546  ellimc2  24581  ellimc3  24583  limcflf  24585  dvmptfsum  24679  dvferm1  24689  dvferm2  24691  dvlip2  24699  c1lip1  24701  lhop1  24718  ftc1a  24741  ply1divex  24841  plyeq0lem  24911  plymullem1  24915  coemullem  24951  coemulc  24956  ulmshftlem  25088  ulmcaulem  25093  ulmbdd  25097  ulmcn  25098  ulmdvlem3  25101  mtestbdd  25104  pserulm  25121  pserdvlem2  25127  abelthlem8  25138  xrlimcnp  25658  jensen  25678  lgamucov  25727  logfac2  25905  dchrelbas3  25926  dchrpt  25955  gausslemma2dlem1a  26053  lgsquad3  26075  2sqb  26120  rpvmasumlem  26175  dchrisumlem1  26177  dchrisumlem3  26179  dchrmusum2  26182  dchrvmasumlem2  26186  dchrisum0flblem1  26196  dchrisum0lem1b  26203  dchrisum0lem1  26204  dchrisum0  26208  mulog2sumlem2  26223  pntlem3  26297  ostth3  26326  istrkgcb  26354  tgbtwndiff  26404  iscgrglt  26412  tgcgrxfr  26416  motcgrg  26442  lnext  26465  tgbtwnconn1  26473  tgbtwnconn3  26475  legval  26482  legtrid  26489  legso  26497  hlcgreu  26516  tglnne  26526  tglineeltr  26529  tglnne0  26538  colline  26547  tglowdim2l  26548  tglowdim2ln  26549  mirreu3  26552  mirbtwnhl  26578  krippenlem  26588  midexlem  26590  perpcom  26611  footexALT  26616  footex  26619  colperpexlem3  26630  colperpex  26631  opphllem  26633  midex  26635  oppne3  26641  opptgdim2  26643  oppnid  26644  opphllem2  26646  opphllem5  26649  opphllem6  26650  oppperpex  26651  outpasch  26653  hlpasch  26654  lnopp2hpgb  26661  hpgerlem  26663  colopp  26667  colhp  26668  lmieu  26682  lnperpex  26701  trgcopy  26702  trgcopyeulem  26703  iscgra1  26708  cgrane1  26710  cgrane2  26711  cgrane3  26712  cgrane4  26713  cgrahl1  26714  cgrahl2  26715  cgracgr  26716  cgraswap  26718  cgracom  26720  cgratr  26721  flatcgra  26722  cgrabtwn  26724  cgrahl  26725  sacgr  26729  acopyeu  26732  cgrg3col4  26751  tgasa1  26756  f1otrg  26769  f1otrge  26770  axeuclidlem  26860  axcontlem2  26863  umgrvad2edg  27107  usgredg2vlem2  27120  pthdepisspth  27628  clwwlkccatlem  27878  clwlkclwwlklem2  27889  3cycld  28067  eupth2lems  28127  eucrctshift  28132  frgr3vlem2  28163  n4cyclfrgr  28180  numclwwlk1lem2f1  28246  numclwwlk2lem1  28265  ubthlem3  28759  chirredlem1  30277  chirredlem3  30279  cdj1i  30320  fnpreimac  30536  xrge0infss  30611  nn0xmulclb  30622  hashxpe  30655  ccatf1  30751  swrdf1  30756  dfmgc2lem  30803  mgcf1o  30811  gsumhashmul  30846  xrge0tsmsd  30847  omndmul2  30868  gsumle  30880  psgnfzto1stlem  30897  cycpmco2  30930  cycpmrn  30940  tocyccntz  30941  cycpmconjslem2  30952  cyc3conja  30954  submarchi  30970  suborng  31044  isarchiofld  31046  imaslmod  31078  znfermltl  31087  lindfpropd  31101  nsgqusf1olem1  31123  rhmpreimaidl  31128  elrspunidl  31131  rhmimaidl  31134  qsidomlem1  31153  mxidlprm  31165  lindsunlem  31230  lindsun  31231  lbsdiflsp0  31232  dimkerim  31233  fedgmul  31237  extdg1id  31263  smatrcl  31271  1smat1  31279  submateq  31284  mdetpmtr1  31298  madjusmdetlem2  31303  locfinreflem  31315  cmppcmp  31333  rhmpreimacn  31360  ordtrest2NEWlem  31397  ordtconnlem1  31399  lmdvg  31428  esumpcvgval  31569  esum2d  31584  sigapildsys  31653  ldgenpisyslem1  31654  fiunelros  31665  volmeas  31722  imambfm  31752  omssubadd  31790  carsggect  31808  carsgclctunlem3  31810  sgnmul  32032  signsply0  32053  signstres  32077  actfunsnf1o  32107  actfunsnrndisj  32108  reprsuc  32118  reprinfz1  32125  breprexplema  32133  breprexplemc  32135  breprexp  32136  breprexpnat  32137  circlemeth  32143  hgt750lemb  32159  tgoldbachgtd  32165  erdszelem8  32680  pconnconn  32713  cvmlift2lem12  32796  cvmlift3lem5  32805  cvmlift3lem7  32807  cvmlift3lem8  32808  mrsubrn  32995  msrval  33020  msubff1  33038  frxp3  33356  slerec  33600  btwnconn1lem13  33976  elicc3  34081  neibastop2lem  34124  unbdqndv2  34266  irrdifflemf  35045  ltflcei  35351  lindsenlbs  35358  matunitlindflem1  35359  matunitlindflem2  35360  poimirlem4  35367  poimirlem13  35376  poimirlem14  35377  poimirlem22  35385  poimirlem26  35389  poimirlem27  35390  heicant  35398  mblfinlem2  35401  mblfinlem3  35402  mblfinlem4  35403  cnambfre  35411  itg2addnclem  35414  itg2addnclem2  35415  itg2gt0cn  35418  ftc1cnnc  35435  ftc1anclem5  35440  ftc1anclem7  35442  ftc1anc  35444  equivtotbnd  35522  isbndx  35526  ssbnd  35532  heibor1lem  35553  rrncmslem  35576  islshpat  36619  lfl1dim  36723  lfl1dim2N  36724  lkrpssN  36765  glbconN  36979  hlhgt2  36991  3dim2  37070  3dim3  37071  islln3  37112  islvol5  37181  2lplnja  37221  dalem19  37284  isline4N  37379  2polssN  37517  lhpmatb  37633  4atex  37678  trlatn0  37774  cdlemf2  38164  dialss  38648  diaglbN  38657  diaintclN  38660  dibglbN  38768  dibintclN  38769  dihlsscpre  38836  dihglblem5aN  38894  dihglblem2aN  38895  dihglblem4  38899  dihatexv  38940  dihjat1lem  39030  lcfl6  39102  mapdval2N  39232  fsuppind  39812  sn-0tie0  39946  prjspertr  39969  prjspreln0  39973  prjspner1  39988  elrfi  40036  eldioph2  40104  diophin  40114  irrapxlem2  40165  irrapxlem3  40166  irrapxlem4  40167  irrapxlem5  40168  pell1234qrne0  40195  pell1234qrreccl  40196  pell1234qrmulcl  40197  pell14qrgt0  40201  pell14qrdich  40211  pell1qrge1  40212  pellfundex  40228  congabseq  40316  jm2.27b  40348  jm2.27  40350  fnwe2lem2  40396  kelac1  40408  lnrfg  40464  hbt  40475  rfovcnvf1od  41106  ntrneiiso  41195  ntrneikb  41198  ntrneixb  41199  ntrneik3  41200  ntrneix3  41201  ntrneik13  41202  ntrneix13  41203  cvgdvgrat  41418  binomcxplemnotnn0  41461  sineq0ALT  42044  disjf1  42207  supxrgere  42361  supxrgelem  42365  supxrge  42366  suplesup  42367  xralrple2  42382  infxr  42395  infleinflem2  42399  infleinf  42400  uzub  42462  mccl  42634  limcrecl  42665  lptioo2  42667  lptioo1  42668  lptre2pt  42676  addlimc  42684  limsupmnflem  42756  climxrre  42786  liminflimsupclim  42843  climxlim2lem  42881  xlimliminflimsup  42898  icccncfext  42923  cncfiooicclem1  42929  cncfiooiccre  42931  dvbdfbdioolem2  42965  ioodvbdlimc1lem1  42967  dvnxpaek  42978  dvmptfprodlem  42980  dvmptfprod  42981  dvnprodlem3  42984  itgioocnicc  43013  itgspltprt  43015  stoweidlem31  43067  fourierdlem39  43182  fourierdlem42  43185  fourierdlem48  43190  fourierdlem49  43191  fourierdlem50  43192  fourierdlem51  43193  fourierdlem64  43206  fourierdlem65  43207  fourierdlem74  43216  fourierdlem75  43217  fourierdlem81  43223  fourierdlem82  43224  fourierdlem101  43243  etransclem23  43293  etransclem27  43297  etransclem32  43302  etransclem33  43303  etransclem35  43305  etransclem38  43308  sge0tsms  43413  sge0cl  43414  sge0f1o  43415  sge0split  43442  sge0rpcpnf  43454  sge0seq  43479  nnfoctbdjlem  43488  iundjiun  43493  meaiuninc3v  43517  meaiininclem  43519  omeiunltfirp  43552  carageniuncllem2  43555  carageniuncl  43556  hoidmv1lelem1  43624  hoidmvlelem3  43630  hoidmvlelem5  43632  hoidmvle  43633  hoiqssbllem3  43657  iunhoiioolem  43708  pimdecfgtioo  43746  pimincfltioo  43747  preimageiingt  43749  preimaleiinlt  43750  smflimlem4  43801  iccpartigtl  44336  iccpartgt  44340  sprsymrelf1lem  44404  paireqne  44424  proththd  44527  requad2  44536  sbgoldbst  44691  bgoldbtbndlem4  44721  isomushgr  44739  isomuspgrlem2d  44744  resmgmhm2b  44815  2zrngmmgm  44965  cznrng  44974  rnghmsubcsetclem2  44995  rhmsubcsetclem2  45041  srhmsubc  45095  rhmsubclem4  45108  srhmsubcALTV  45113  rhmsubcALTVlem4  45126  lincsum  45231  lcoss  45238  snlindsntor  45273  islindeps2  45285  line2x  45561  line2y  45562  itscnhlinecirc02p  45592