Theorem ad3antrrr 727

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 723	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 206  df-an 396

This theorem is referenced by:  ad4antr  729  ad4antlr  730  ad5ant12  753  simplll  772  fsnex  7284  fimaproj  8124  frxp3  8140  oaabs  8650  oaabs2  8651  omabs  8653  cofon1  8674  undomOLD  9063  sbthlem8  9093  findcard3OLD  9289  cantnfle  9669  cantnfp1  9679  cantnflem1c  9685  sornom  10275  enfin2i  10319  ttukeylem6  10512  fpwwe2lem12  10640  winalim2  10694  wuncval2  10745  negf1o  11649  xlemul1a  13272  difreicc  13466  flflp1  13777  faclbnd  14255  swrdswrd  14660  pfxccatin12lem3  14687  swrdccat3blem  14694  ello12  15465  elo12  15476  rlimclim1  15494  rlimcld2  15527  o1co  15535  o1of2  15562  o1rlimmul  15568  rlimsqzlem  15600  isercoll  15619  o1fsum  15764  supcvg  15807  dvds2ln  16237  lcmgcdlem  16548  cncongr2  16610  isprm5  16649  prmdvdsncoprmbd  16668  pcadd  16827  vdwlem2  16920  vdwlem11  16929  sbcie3s  17100  prdsval  17406  mreexexlem4d  17596  isacs2  17602  catcocl  17634  catass  17635  subccocl  17800  fullsubc  17805  funcco  17826  fullpropd  17876  ffthiso  17885  isnat  17903  natpropd  17934  fucpropd  17935  xpcval  18134  evlf2  18176  curfpropd  18191  curfuncf  18196  uncfcurf  18197  hofcl  18217  hofpropd  18225  yonffthlem  18240  isacs3lem  18500  acsfiindd  18511  gsumpropd2lem  18605  resmgmhm2b  18639  resmhm2b  18740  mhmid  18983  mhmmnd  18984  ghmgrp  18986  conjnmzb  19168  pgpfi  19515  sylow3lem2  19538  efgredlem  19657  frgpnabllem1  19783  imasabl  19786  dprdfcntz  19927  ablfac1b  19982  pgpfac1lem3  19989  pgpfac1lem5  19991  pgpfaclem3  19995  ringinvnzdiv  20190  imadrhmcl  20557  cntzsdrg  20562  islmhm2  20794  lspsneleq  20874  znunit  21339  psgndiflemB  21373  uvcff  21566  uvcf1  21567  lindfmm  21602  sraassab  21642  psrval  21688  psrass1  21745  resspsrmul  21757  mplbas2  21817  mhpmulcl  21912  coe1tmmul  22020  gsummoncoe1  22049  dmatsubcl  22221  scmatscm  22236  smatvscl  22247  marrepval  22285  mdetdiaglem  22321  mdetunilem8  22342  mdetunilem9  22343  pmatcoe1fsupp  22424  decpmatmulsumfsupp  22496  pmatcollpw2lem  22500  mp2pm2mplem4  22532  pm2mpmhmlem1  22541  pm2mpmhmlem2  22542  pm2mp  22548  fvmptnn04if  22572  cpmadugsumfi  22600  cpmidg2sum  22603  cpmadumatpoly  22606  cayhamlem4  22611  neiptoptop  22856  neitr  22905  ordtrest2lem  22928  cnpnei  22989  iscncl  22994  cncls  22999  cnntr  23000  cncnp  23005  lmcnp  23029  isreg2  23102  hauscmplem  23131  cmpfi  23133  1stcfb  23170  1stcrest  23178  2ndcctbss  23180  2ndcomap  23183  islly2  23209  cldllycmp  23220  lly1stc  23221  locfincmp  23251  llycmpkgen2  23275  1stckgenlem  23278  kgencn2  23282  kgencn3  23283  ptbasfi  23306  ptpjopn  23337  txdis1cn  23360  txlly  23361  txnlly  23362  txtube  23365  txcmplem2  23367  tx1stc  23375  txkgen  23377  xkopt  23380  xkoco2cn  23383  xkococnlem  23384  xkococn  23385  xkoinjcn  23412  tgqtop  23437  regr1lem  23464  kqreglem1  23466  nrmhmph  23519  rnelfmlem  23677  rnelfm  23678  fmfnfmlem4  23682  fmfnfm  23683  ufldom  23687  flimopn  23700  hauspwpwf1  23712  fclsopn  23739  fclsnei  23744  fclsrest  23749  alexsublem  23769  alexsubALTlem3  23774  ptcmplem2  23778  ptcmplem3  23779  cnextfun  23789  cnextcn  23792  symgtgp  23831  tgpt0  23844  qustgpopn  23845  tsmsxplem1  23878  trust  23955  utopsnneiplem  23973  utop3cls  23977  utopreg  23978  isucn2  24005  cstucnd  24010  ucncn  24011  fmucnd  24018  cfilufg  24019  neipcfilu  24022  met2ndci  24252  prdsxmslem2  24259  metustid  24284  metustexhalf  24286  metust  24288  psmetutop  24297  nmoleub  24469  reconnlem2  24564  xrge0tsms  24571  cncfco  24648  lebnumlem3  24710  lebnum  24711  nmoleub2lem2  24864  nmoleub3  24867  iscfil2  25015  iscau4  25028  iscmet3lem2  25041  equivcfil  25048  equivcau  25049  caubl  25057  rrxdstprj1  25158  ovolshftlem2  25260  ovolicc2lem4  25270  uniioombl  25339  i1fmulclem  25453  mbfi1fseqlem6  25471  itg2const2  25492  itg2split  25500  bddiblnc  25592  ellimc2  25627  ellimc3  25629  limcflf  25631  dvmptfsum  25725  dvferm1  25735  dvferm2  25737  dvlip2  25745  c1lip1  25747  lhop1  25764  ftc1a  25787  ply1divex  25887  plyeq0lem  25957  plymullem1  25961  coemullem  25997  coemulc  26002  ulmshftlem  26134  ulmcaulem  26139  ulmbdd  26143  ulmcn  26144  ulmdvlem3  26147  mtestbdd  26150  pserulm  26167  pserdvlem2  26173  abelthlem8  26184  xrlimcnp  26706  jensen  26726  lgamucov  26775  logfac2  26953  dchrelbas3  26974  dchrpt  27003  gausslemma2dlem1a  27101  lgsquad3  27123  2sqb  27168  rpvmasumlem  27223  dchrisumlem1  27225  dchrisumlem3  27227  dchrmusum2  27230  dchrvmasumlem2  27234  dchrisum0flblem1  27244  dchrisum0lem1b  27251  dchrisum0lem1  27252  dchrisum0  27256  mulog2sumlem2  27271  pntlem3  27345  ostth3  27374  slerec  27554  cofcutr  27646  istrkgcb  27971  tgbtwndiff  28021  iscgrglt  28029  tgcgrxfr  28033  motcgrg  28059  lnext  28082  tgbtwnconn1  28090  tgbtwnconn3  28092  legval  28099  legtrid  28106  legso  28114  hlcgreu  28133  tglnne  28143  tglineeltr  28146  tglnne0  28155  colline  28164  tglowdim2l  28165  tglowdim2ln  28166  mirreu3  28169  mirbtwnhl  28195  krippenlem  28205  midexlem  28207  perpcom  28228  footexALT  28233  footex  28236  colperpexlem3  28247  colperpex  28248  opphllem  28250  midex  28252  oppne3  28258  opptgdim2  28260  oppnid  28261  opphllem2  28263  opphllem5  28266  opphllem6  28267  oppperpex  28268  outpasch  28270  hlpasch  28271  lnopp2hpgb  28278  hpgerlem  28280  colopp  28284  colhp  28285  lmieu  28299  lnperpex  28318  trgcopy  28319  trgcopyeulem  28320  iscgra1  28325  cgrane1  28327  cgrane2  28328  cgrane3  28329  cgrane4  28330  cgrahl1  28331  cgrahl2  28332  cgracgr  28333  cgraswap  28335  cgracom  28337  cgratr  28338  flatcgra  28339  cgrabtwn  28341  cgrahl  28342  sacgr  28346  acopyeu  28349  cgrg3col4  28368  tgasa1  28373  f1otrg  28386  f1otrge  28387  axeuclidlem  28484  axcontlem2  28487  umgrvad2edg  28734  usgredg2vlem2  28747  pthdepisspth  29256  clwwlkccatlem  29506  clwlkclwwlklem2  29517  3cycld  29695  eupth2lems  29755  eucrctshift  29760  frgr3vlem2  29791  n4cyclfrgr  29808  numclwwlk1lem2f1  29874  numclwwlk2lem1  29893  ubthlem3  30389  chirredlem1  31907  chirredlem3  31909  cdj1i  31950  fnpreimac  32160  xrge0infss  32237  nn0xmulclb  32248  hashxpe  32283  ccatf1  32379  swrdf1  32384  dfmgc2lem  32429  mgcf1o  32437  gsumhashmul  32475  xrge0tsmsd  32476  omndmul2  32497  gsumle  32509  psgnfzto1stlem  32526  cycpmco2  32559  cycpmrn  32569  tocyccntz  32570  cycpmconjslem2  32581  cyc3conja  32583  submarchi  32599  suborng  32700  isarchiofld  32702  imaslmod  32735  znfermltl  32750  lindfpropd  32769  nsgqusf1olem1  32795  ghmquskerlem3  32802  ghmqusker  32803  rhmpreimaidl  32808  unitpidl1  32813  elrspunidl  32817  elrspunsn  32818  rhmimaidl  32821  drngidl  32822  qsidomlem1  32842  mxidlprm  32857  mxidlirredi  32858  qsdrngilem  32879  qsdrngi  32880  evls1fpws  32917  ply1degltdimlem  32992  lindsunlem  32994  lindsun  32995  lbsdiflsp0  32996  dimkerim  32997  fedgmul  33001  extdg1id  33027  evls1fldgencl  33030  minplyirred  33056  smatrcl  33071  1smat1  33079  submateq  33084  mdetpmtr1  33098  madjusmdetlem2  33103  locfinreflem  33115  cmppcmp  33133  rhmpreimacn  33160  ordtrest2NEWlem  33197  ordtconnlem1  33199  lmdvg  33228  esumpcvgval  33371  esum2d  33386  sigapildsys  33455  ldgenpisyslem1  33456  fiunelros  33467  volmeas  33524  imambfm  33556  omssubadd  33594  carsggect  33612  carsgclctunlem3  33614  sgnmul  33836  signsply0  33857  signstres  33881  actfunsnf1o  33911  actfunsnrndisj  33912  reprsuc  33922  reprinfz1  33929  breprexplema  33937  breprexplemc  33939  breprexp  33940  breprexpnat  33941  circlemeth  33947  hgt750lemb  33963  tgoldbachgtd  33969  erdszelem8  34484  pconnconn  34517  cvmlift2lem12  34600  cvmlift3lem5  34609  cvmlift3lem7  34611  cvmlift3lem8  34612  mrsubrn  34799  msrval  34824  msubff1  34842  btwnconn1lem13  35372  elicc3  35506  neibastop2lem  35549  unbdqndv2  35691  irrdifflemf  36510  ltflcei  36780  lindsenlbs  36787  matunitlindflem1  36788  matunitlindflem2  36789  poimirlem4  36796  poimirlem13  36805  poimirlem14  36806  poimirlem22  36814  poimirlem26  36818  poimirlem27  36819  heicant  36827  mblfinlem2  36830  mblfinlem3  36831  mblfinlem4  36832  cnambfre  36840  itg2addnclem  36843  itg2addnclem2  36844  itg2gt0cn  36847  ftc1cnnc  36864  ftc1anclem5  36869  ftc1anclem7  36871  ftc1anc  36873  equivtotbnd  36950  isbndx  36954  ssbnd  36960  heibor1lem  36981  rrncmslem  37004  islshpat  38191  lfl1dim  38295  lfl1dim2N  38296  lkrpssN  38337  glbconN  38551  glbconNOLD  38552  hlhgt2  38564  3dim2  38643  3dim3  38644  islln3  38685  islvol5  38754  2lplnja  38794  dalem19  38857  isline4N  38952  2polssN  39090  lhpmatb  39206  4atex  39251  trlatn0  39347  cdlemf2  39737  dialss  40221  diaglbN  40230  diaintclN  40233  dibglbN  40341  dibintclN  40342  dihlsscpre  40409  dihglblem5aN  40467  dihglblem2aN  40468  dihglblem4  40472  dihatexv  40513  dihjat1lem  40603  lcfl6  40675  mapdval2N  40805  aks4d1p8  41259  fldhmf1  41262  sticksstones8  41276  sticksstones12a  41280  imacrhmcl  41394  evlsvvval  41438  evlselv  41462  fsuppind  41465  sn-0tie0  41615  prjspertr  41650  prjspreln0  41654  prjspner1  41671  elrfi  41735  eldioph2  41803  diophin  41813  irrapxlem2  41864  irrapxlem3  41865  irrapxlem4  41866  irrapxlem5  41867  pell1234qrne0  41894  pell1234qrreccl  41895  pell1234qrmulcl  41896  pell14qrgt0  41900  pell14qrdich  41910  pell1qrge1  41911  pellfundex  41927  congabseq  42016  jm2.27b  42048  jm2.27  42050  fnwe2lem2  42096  kelac1  42108  lnrfg  42164  hbt  42175  nadd1suc  42445  rfovcnvf1od  43058  ntrneiiso  43145  ntrneikb  43148  ntrneixb  43149  ntrneik3  43150  ntrneix3  43151  ntrneik13  43152  ntrneix13  43153  cvgdvgrat  43375  binomcxplemnotnn0  43418  sineq0ALT  44001  disjf1  44182  supxrgere  44343  supxrgelem  44347  supxrge  44348  suplesup  44349  xralrple2  44364  infxr  44377  infleinflem2  44381  infleinf  44382  uzub  44441  mccl  44614  limcrecl  44645  lptioo2  44647  lptioo1  44648  lptre2pt  44656  addlimc  44664  limsupmnflem  44736  climxrre  44766  liminflimsupclim  44823  climxlim2lem  44861  xlimliminflimsup  44878  icccncfext  44903  cncfiooicclem1  44909  cncfiooiccre  44911  dvbdfbdioolem2  44945  ioodvbdlimc1lem1  44947  dvnxpaek  44958  dvmptfprodlem  44960  dvmptfprod  44961  dvnprodlem3  44964  itgioocnicc  44993  itgspltprt  44995  stoweidlem31  45047  fourierdlem39  45162  fourierdlem42  45165  fourierdlem48  45170  fourierdlem49  45171  fourierdlem50  45172  fourierdlem51  45173  fourierdlem64  45186  fourierdlem65  45187  fourierdlem74  45196  fourierdlem75  45197  fourierdlem81  45203  fourierdlem82  45204  fourierdlem101  45223  etransclem23  45273  etransclem27  45277  etransclem32  45282  etransclem33  45283  etransclem35  45285  etransclem38  45288  sge0tsms  45396  sge0cl  45397  sge0f1o  45398  sge0split  45425  sge0rpcpnf  45437  sge0seq  45462  nnfoctbdjlem  45471  iundjiun  45476  meaiuninc3v  45500  meaiininclem  45502  omeiunltfirp  45535  carageniuncllem2  45538  carageniuncl  45539  hoidmv1lelem1  45607  hoidmvlelem3  45613  hoidmvlelem5  45615  hoidmvle  45616  hoiqssbllem3  45640  iunhoiioolem  45691  pimdecfgtioo  45733  pimincfltioo  45734  preimageiingt  45736  preimaleiinlt  45737  smflimlem4  45790  iccpartigtl  46391  iccpartgt  46395  sprsymrelf1lem  46459  paireqne  46479  proththd  46582  requad2  46591  sbgoldbst  46746  bgoldbtbndlem4  46776  isomushgr  46794  isomuspgrlem2d  46799  2zrngmmgm  46934  cznrng  46943  rnghmsubcsetclem2  46964  rhmsubcsetclem2  47010  srhmsubc  47064  rhmsubclem4  47077  srhmsubcALTV  47082  rhmsubcALTVlem4  47095  lincsum  47199  lcoss  47206  snlindsntor  47241  islindeps2  47253  line2x  47529  line2y  47530  itscnhlinecirc02p  47560