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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad4antr  729  ad4antlr  730  ad5ant12  753  simplll  772  fsnex  7164  fimaproj  7985  oaabs  8487  oaabs2  8488  omabs  8490  undomOLD  8856  sbthlem8  8886  findcard3  9066  cantnfle  9438  cantnfp1  9448  cantnflem1c  9454  sornom  10042  enfin2i  10086  ttukeylem6  10279  fpwwe2lem12  10407  winalim2  10461  wuncval2  10512  negf1o  11414  xlemul1a  13031  difreicc  13225  flflp1  13536  faclbnd  14013  swrdswrd  14427  pfxccatin12lem3  14454  swrdccat3blem  14461  ello12  15234  elo12  15245  rlimclim1  15263  rlimcld2  15296  o1co  15304  o1of2  15331  o1rlimmul  15337  rlimsqzlem  15369  isercoll  15388  o1fsum  15534  supcvg  15577  dvds2ln  16007  lcmgcdlem  16320  cncongr2  16382  isprm5  16421  prmdvdsncoprmbd  16440  pcadd  16599  vdwlem2  16692  vdwlem11  16701  sbcie3s  16872  prdsval  17175  mreexexlem4d  17365  isacs2  17371  catcocl  17403  catass  17404  subccocl  17569  fullsubc  17574  funcco  17595  fullpropd  17645  ffthiso  17654  isnat  17672  natpropd  17703  fucpropd  17704  xpcval  17903  evlf2  17945  curfpropd  17960  curfuncf  17965  uncfcurf  17966  hofcl  17986  hofpropd  17994  yonffthlem  18009  isacs3lem  18269  acsfiindd  18280  gsumpropd2lem  18372  resmhm2b  18470  mhmid  18705  mhmmnd  18706  ghmgrp  18708  conjnmzb  18878  pgpfi  19219  sylow3lem2  19242  efgredlem  19362  frgpnabllem1  19483  dprdfcntz  19627  ablfac1b  19682  pgpfac1lem3  19689  pgpfac1lem5  19691  pgpfaclem3  19695  ringinvnzdiv  19841  cntzsdrg  20079  islmhm2  20309  lspsneleq  20386  znunit  20780  psgndiflemB  20814  uvcff  21007  uvcf1  21008  lindfmm  21043  psrval  21127  psrass1  21183  resspsrmul  21195  mplbas2  21252  mhpmulcl  21348  coe1tmmul  21457  gsummoncoe1  21484  dmatsubcl  21656  scmatscm  21671  smatvscl  21682  marrepval  21720  mdetdiaglem  21756  mdetunilem8  21777  mdetunilem9  21778  pmatcoe1fsupp  21859  decpmatmulsumfsupp  21931  pmatcollpw2lem  21935  mp2pm2mplem4  21967  pm2mpmhmlem1  21976  pm2mpmhmlem2  21977  pm2mp  21983  fvmptnn04if  22007  cpmadugsumfi  22035  cpmidg2sum  22038  cpmadumatpoly  22041  cayhamlem4  22046  neiptoptop  22291  neitr  22340  ordtrest2lem  22363  cnpnei  22424  iscncl  22429  cncls  22434  cnntr  22435  cncnp  22440  lmcnp  22464  isreg2  22537  hauscmplem  22566  cmpfi  22568  1stcfb  22605  1stcrest  22613  2ndcctbss  22615  2ndcomap  22618  islly2  22644  cldllycmp  22655  lly1stc  22656  locfincmp  22686  llycmpkgen2  22710  1stckgenlem  22713  kgencn2  22717  kgencn3  22718  ptbasfi  22741  ptpjopn  22772  txdis1cn  22795  txlly  22796  txnlly  22797  txtube  22800  txcmplem2  22802  tx1stc  22810  txkgen  22812  xkopt  22815  xkoco2cn  22818  xkococnlem  22819  xkococn  22820  xkoinjcn  22847  tgqtop  22872  regr1lem  22899  kqreglem1  22901  nrmhmph  22954  rnelfmlem  23112  rnelfm  23113  fmfnfmlem4  23117  fmfnfm  23118  ufldom  23122  flimopn  23135  hauspwpwf1  23147  fclsopn  23174  fclsnei  23179  fclsrest  23184  alexsublem  23204  alexsubALTlem3  23209  ptcmplem2  23213  ptcmplem3  23214  cnextfun  23224  cnextcn  23227  symgtgp  23266  tgpt0  23279  qustgpopn  23280  tsmsxplem1  23313  trust  23390  utopsnneiplem  23408  utop3cls  23412  utopreg  23413  isucn2  23440  cstucnd  23445  ucncn  23446  fmucnd  23453  cfilufg  23454  neipcfilu  23457  met2ndci  23687  prdsxmslem2  23694  metustid  23719  metustexhalf  23721  metust  23723  psmetutop  23732  nmoleub  23904  reconnlem2  23999  xrge0tsms  24006  cncfco  24079  lebnumlem3  24135  lebnum  24136  nmoleub2lem2  24288  nmoleub3  24291  iscfil2  24439  iscau4  24452  iscmet3lem2  24465  equivcfil  24472  equivcau  24473  caubl  24481  rrxdstprj1  24582  ovolshftlem2  24683  ovolicc2lem4  24693  uniioombl  24762  i1fmulclem  24876  mbfi1fseqlem6  24894  itg2const2  24915  itg2split  24923  bddiblnc  25015  ellimc2  25050  ellimc3  25052  limcflf  25054  dvmptfsum  25148  dvferm1  25158  dvferm2  25160  dvlip2  25168  c1lip1  25170  lhop1  25187  ftc1a  25210  ply1divex  25310  plyeq0lem  25380  plymullem1  25384  coemullem  25420  coemulc  25425  ulmshftlem  25557  ulmcaulem  25562  ulmbdd  25566  ulmcn  25567  ulmdvlem3  25570  mtestbdd  25573  pserulm  25590  pserdvlem2  25596  abelthlem8  25607  xrlimcnp  26127  jensen  26147  lgamucov  26196  logfac2  26374  dchrelbas3  26395  dchrpt  26424  gausslemma2dlem1a  26522  lgsquad3  26544  2sqb  26589  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem2  26655  dchrisum0flblem1  26665  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0  26677  mulog2sumlem2  26692  pntlem3  26766  ostth3  26795  istrkgcb  26826  tgbtwndiff  26876  iscgrglt  26884  tgcgrxfr  26888  motcgrg  26914  lnext  26937  tgbtwnconn1  26945  tgbtwnconn3  26947  legval  26954  legtrid  26961  legso  26969  hlcgreu  26988  tglnne  26998  tglineeltr  27001  tglnne0  27010  colline  27019  tglowdim2l  27020  tglowdim2ln  27021  mirreu3  27024  mirbtwnhl  27050  krippenlem  27060  midexlem  27062  perpcom  27083  footexALT  27088  footex  27091  colperpexlem3  27102  colperpex  27103  opphllem  27105  midex  27107  oppne3  27113  opptgdim2  27115  oppnid  27116  opphllem2  27118  opphllem5  27121  opphllem6  27122  oppperpex  27123  outpasch  27125  hlpasch  27126  lnopp2hpgb  27133  hpgerlem  27135  colopp  27139  colhp  27140  lmieu  27154  lnperpex  27173  trgcopy  27174  trgcopyeulem  27175  iscgra1  27180  cgrane1  27182  cgrane2  27183  cgrane3  27184  cgrane4  27185  cgrahl1  27186  cgrahl2  27187  cgracgr  27188  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  cgrabtwn  27196  cgrahl  27197  sacgr  27201  acopyeu  27204  cgrg3col4  27223  tgasa1  27228  f1otrg  27241  f1otrge  27242  axeuclidlem  27339  axcontlem2  27342  umgrvad2edg  27589  usgredg2vlem2  27602  pthdepisspth  28112  clwwlkccatlem  28362  clwlkclwwlklem2  28373  3cycld  28551  eupth2lems  28611  eucrctshift  28616  frgr3vlem2  28647  n4cyclfrgr  28664  numclwwlk1lem2f1  28730  numclwwlk2lem1  28749  ubthlem3  29243  chirredlem1  30761  chirredlem3  30763  cdj1i  30804  fnpreimac  31017  xrge0infss  31092  nn0xmulclb  31103  hashxpe  31136  ccatf1  31232  swrdf1  31237  dfmgc2lem  31282  mgcf1o  31290  gsumhashmul  31325  xrge0tsmsd  31326  omndmul2  31347  gsumle  31359  psgnfzto1stlem  31376  cycpmco2  31409  cycpmrn  31419  tocyccntz  31420  cycpmconjslem2  31431  cyc3conja  31433  submarchi  31449  suborng  31523  isarchiofld  31525  imaslmod  31562  znfermltl  31571  lindfpropd  31585  nsgqusf1olem1  31607  rhmpreimaidl  31612  elrspunidl  31615  rhmimaidl  31618  qsidomlem1  31637  mxidlprm  31649  lindsunlem  31714  lindsun  31715  lbsdiflsp0  31716  dimkerim  31717  fedgmul  31721  extdg1id  31747  smatrcl  31755  1smat1  31763  submateq  31768  mdetpmtr1  31782  madjusmdetlem2  31787  locfinreflem  31799  cmppcmp  31817  rhmpreimacn  31844  ordtrest2NEWlem  31881  ordtconnlem1  31883  lmdvg  31912  esumpcvgval  32055  esum2d  32070  sigapildsys  32139  ldgenpisyslem1  32140  fiunelros  32151  volmeas  32208  imambfm  32238  omssubadd  32276  carsggect  32294  carsgclctunlem3  32296  sgnmul  32518  signsply0  32539  signstres  32563  actfunsnf1o  32593  actfunsnrndisj  32594  reprsuc  32604  reprinfz1  32611  breprexplema  32619  breprexplemc  32621  breprexp  32622  breprexpnat  32623  circlemeth  32629  hgt750lemb  32645  tgoldbachgtd  32651  erdszelem8  33169  pconnconn  33202  cvmlift2lem12  33285  cvmlift3lem5  33294  cvmlift3lem7  33296  cvmlift3lem8  33297  mrsubrn  33484  msrval  33509  msubff1  33527  frxp3  33806  slerec  34022  cofcutr  34101  btwnconn1lem13  34410  elicc3  34515  neibastop2lem  34558  unbdqndv2  34700  irrdifflemf  35505  ltflcei  35774  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem4  35790  poimirlem13  35799  poimirlem14  35800  poimirlem22  35808  poimirlem26  35812  poimirlem27  35813  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  cnambfre  35834  itg2addnclem  35837  itg2addnclem2  35838  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anc  35867  equivtotbnd  35945  isbndx  35949  ssbnd  35955  heibor1lem  35976  rrncmslem  35999  islshpat  37038  lfl1dim  37142  lfl1dim2N  37143  lkrpssN  37184  glbconN  37398  hlhgt2  37410  3dim2  37489  3dim3  37490  islln3  37531  islvol5  37600  2lplnja  37640  dalem19  37703  isline4N  37798  2polssN  37936  lhpmatb  38052  4atex  38097  trlatn0  38193  cdlemf2  38583  dialss  39067  diaglbN  39076  diaintclN  39079  dibglbN  39187  dibintclN  39188  dihlsscpre  39255  dihglblem5aN  39313  dihglblem2aN  39314  dihglblem4  39318  dihatexv  39359  dihjat1lem  39449  lcfl6  39521  mapdval2N  39651  aks4d1p8  40102  sticksstones8  40116  sticksstones12a  40120  fsuppind  40286  sn-0tie0  40428  prjspertr  40451  prjspreln0  40455  prjspner1  40470  elrfi  40523  eldioph2  40591  diophin  40601  irrapxlem2  40652  irrapxlem3  40653  irrapxlem4  40654  irrapxlem5  40655  pell1234qrne0  40682  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell14qrgt0  40688  pell14qrdich  40698  pell1qrge1  40699  pellfundex  40715  congabseq  40803  jm2.27b  40835  jm2.27  40837  fnwe2lem2  40883  kelac1  40895  lnrfg  40951  hbt  40962  rfovcnvf1od  41619  ntrneiiso  41708  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  cvgdvgrat  41938  binomcxplemnotnn0  41981  sineq0ALT  42564  disjf1  42727  supxrgere  42879  supxrgelem  42883  supxrge  42884  suplesup  42885  xralrple2  42900  infxr  42913  infleinflem2  42917  infleinf  42918  uzub  42978  mccl  43146  limcrecl  43177  lptioo2  43179  lptioo1  43180  lptre2pt  43188  addlimc  43196  limsupmnflem  43268  climxrre  43298  liminflimsupclim  43355  climxlim2lem  43393  xlimliminflimsup  43410  icccncfext  43435  cncfiooicclem1  43441  cncfiooiccre  43443  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  dvnxpaek  43490  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem3  43496  itgioocnicc  43525  itgspltprt  43527  stoweidlem31  43579  fourierdlem39  43694  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem64  43718  fourierdlem65  43719  fourierdlem74  43728  fourierdlem75  43729  fourierdlem81  43735  fourierdlem82  43736  fourierdlem101  43755  etransclem23  43805  etransclem27  43809  etransclem32  43814  etransclem33  43815  etransclem35  43817  etransclem38  43820  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0split  43954  sge0rpcpnf  43966  sge0seq  43991  nnfoctbdjlem  44000  iundjiun  44005  meaiuninc3v  44029  meaiininclem  44031  omeiunltfirp  44064  carageniuncllem2  44067  carageniuncl  44068  hoidmv1lelem1  44136  hoidmvlelem3  44142  hoidmvlelem5  44144  hoidmvle  44145  hoiqssbllem3  44169  iunhoiioolem  44220  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  smflimlem4  44319  iccpartigtl  44886  iccpartgt  44890  sprsymrelf1lem  44954  paireqne  44974  proththd  45077  requad2  45086  sbgoldbst  45241  bgoldbtbndlem4  45271  isomushgr  45289  isomuspgrlem2d  45294  resmgmhm2b  45365  2zrngmmgm  45515  cznrng  45524  rnghmsubcsetclem2  45545  rhmsubcsetclem2  45591  srhmsubc  45645  rhmsubclem4  45658  srhmsubcALTV  45663  rhmsubcALTVlem4  45676  lincsum  45781  lcoss  45788  snlindsntor  45823  islindeps2  45835  line2x  46111  line2y  46112  itscnhlinecirc02p  46142