Theorem ad3antrrr 721

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  ad4antr  724  ad4antrOLD  725  ad4antlr  726  ad5ant12  766  simplll  791  simp-4r  803  fsnex  6730  oaabs  7929  oaabs2  7930  omabs  7932  undom  8255  sbthlem8  8284  findcard3  8410  cantnfle  8783  cantnfp1  8793  cantnflem1c  8799  sornom  9352  enfin2i  9396  ttukeylem6  9589  fpwwe2lem13  9717  fpwwe2  9718  winalim2  9771  wuncval2  9822  negf1o  10714  xlemul1a  12320  difreicc  12511  flflp1  12816  faclbnd  13281  swrdswrd  13692  swrdccatin12lem3  13738  swrdccat3blem  13749  ello12  14532  lo1bdd2  14540  elo12  14543  rlimclim1  14561  rlimcld2  14594  o1co  14602  o1of2  14628  o1rlimmul  14634  rlimsqzlem  14664  isercoll  14683  o1fsum  14829  supcvg  14872  dvds2ln  15299  lcmgcdlem  15600  cncongr2  15662  isprm5  15698  pcadd  15872  vdwlem2  15965  vdwlem11  15974  sbcie3s  16189  prdsval  16381  mreexexlem4d  16573  isacs2  16579  catcocl  16611  catass  16612  subccocl  16770  fullsubc  16775  funcco  16796  funcpropd  16825  fullpropd  16845  ffthiso  16854  isnat  16872  natpropd  16901  fucpropd  16902  xpcval  17083  evlf2  17124  curfpropd  17139  curfuncf  17144  uncfcurf  17145  curf2ndf  17153  hofcl  17165  hofpropd  17173  yonffthlem  17188  isacs3lem  17432  acsfiindd  17443  gsumpropd2lem  17539  resmhm2b  17627  mhmid  17803  mhmmnd  17804  ghmgrp  17806  conjnmzb  17959  pgpfi  18284  sylow3lem2  18307  efgredlem  18425  efgredlemOLD  18426  frgpnabllem1  18542  dprdfcntz  18681  ablfac1b  18736  pgpfac1lem3  18743  pgpfac1lem5  18745  pgpfaclem3  18749  ringinvnzdiv  18860  islmhm2  19310  lspsneleq  19387  psrval  19636  psrass1  19679  resspsrmul  19691  mplbas2  19744  coe1tmmul  19920  gsummoncoe1  19947  znunit  20184  psgndiflemB  20219  uvcff  20406  uvcf1  20407  lindfmm  20442  dmatsubcl  20581  scmatscm  20596  smatvscl  20607  marrepval  20645  mdetdiaglem  20681  mdetunilem8  20702  mdetunilem9  20703  pmatcoe1fsupp  20785  decpmatmulsumfsupp  20857  pmatcollpw2lem  20861  mp2pm2mplem4  20893  pm2mpmhmlem1  20902  pm2mpmhmlem2  20903  pm2mp  20909  fvmptnn04if  20933  cpmadugsumfi  20961  cpmidg2sum  20964  cpmadumatpoly  20967  cayhamlem4  20972  neiptoptop  21215  neitr  21264  ordtrest2lem  21287  cnpnei  21348  iscncl  21353  cncls  21358  cnntr  21359  cncnp  21364  lmcnp  21388  isreg2  21461  hauscmplem  21489  cmpfi  21491  1stcfb  21528  1stcrest  21536  2ndcctbss  21538  2ndcomap  21541  islly2  21567  cldllycmp  21578  lly1stc  21579  locfincmp  21609  llycmpkgen2  21633  1stckgenlem  21636  kgencn2  21640  kgencn3  21641  ptbasfi  21664  ptpjopn  21695  txdis1cn  21718  txlly  21719  txnlly  21720  txtube  21723  txcmplem2  21725  tx1stc  21733  txkgen  21735  xkopt  21738  xkoco2cn  21741  xkococnlem  21742  xkococn  21743  xkoinjcn  21770  tgqtop  21795  regr1lem  21822  kqreglem1  21824  nrmhmph  21877  rnelfmlem  22035  rnelfm  22036  fmfnfmlem4  22040  fmfnfm  22041  ufldom  22045  flimopn  22058  hauspwpwf1  22070  fclsopn  22097  fclsnei  22102  fclsrest  22107  alexsublem  22127  alexsubALTlem3  22132  ptcmplem2  22136  ptcmplem3  22137  cnextfun  22147  cnextcn  22150  symgtgp  22184  tgpt0  22201  qustgpopn  22202  tsmsxplem1  22235  trust  22312  utopsnneiplem  22330  utop3cls  22334  utopreg  22335  isucn2  22362  cstucnd  22367  ucncn  22368  fmucnd  22375  cfilufg  22376  neipcfilu  22379  met2ndci  22606  prdsxmslem2  22613  metcnp3  22624  metustid  22638  metustexhalf  22640  metust  22642  psmetutop  22651  nmoleub  22814  reconnlem2  22909  xrge0tsms  22916  cncfco  22989  lebnumlem3  23041  lebnum  23042  nmoleub2lem2  23194  nmoleub3  23197  iscfil2  23343  iscau4  23356  iscmet3lem2  23369  equivcfil  23376  equivcau  23377  caubl  23385  rrxdstprj1  23481  ovolshftlem2  23568  ovolicc2lem4  23578  uniioombl  23647  i1fmulclem  23760  mbfi1fseqlem6  23778  itg2const2  23799  itg2split  23807  ellimc2  23932  ellimc3  23934  limcflf  23936  dvmptfsum  24029  dvferm1  24039  dvferm2  24041  dvlip2  24049  c1lip1  24051  lhop1  24068  ftc1a  24091  ply1divex  24187  plyeq0lem  24257  plymullem1  24261  coemullem  24297  coemulc  24302  ulmshftlem  24434  ulmcaulem  24439  ulmbdd  24443  ulmcn  24444  ulmdvlem3  24447  mtestbdd  24450  pserulm  24467  pserdvlem2  24473  abelthlem8  24484  xrlimcnp  24986  jensen  25006  lgamucov  25055  logfac2  25233  dchrelbas3  25254  dchrpt  25283  gausslemma2dlem1a  25381  lgsquad3  25403  2sqb  25448  rpvmasumlem  25467  dchrisumlem1  25469  dchrisumlem3  25471  dchrmusum2  25474  dchrvmasumlem2  25478  dchrisum0flblem1  25488  dchrisum0lem1b  25495  dchrisum0lem1  25496  dchrisum0  25500  mulog2sumlem2  25515  pntlem3  25589  ostth3  25618  istrkgcb  25646  tgbtwndiff  25692  iscgrglt  25700  tgcgrxfr  25704  motcgrg  25730  lnext  25753  tgbtwnconn1  25761  tgbtwnconn3  25763  legval  25770  legtrid  25777  legso  25785  hlcgreu  25804  tglnne  25814  tglineeltr  25817  tglnne0  25826  colline  25835  tglowdim2l  25836  tglowdim2ln  25837  mirreu3  25840  mirbtwnhl  25866  krippenlem  25876  midexlem  25878  perpcom  25899  perpneq  25900  footex  25904  colperpexlem3  25915  colperpex  25916  opphllem  25918  midex  25920  oppne3  25926  opptgdim2  25928  oppnid  25929  opphllem2  25931  opphllem5  25934  opphllem6  25935  oppperpex  25936  outpasch  25938  hlpasch  25939  lnopp2hpgb  25946  hpgerlem  25948  colopp  25952  colhp  25953  lmieu  25967  lnperpex  25986  trgcopy  25987  trgcopyeulem  25988  iscgra1  25993  cgrane1  25995  cgrane2  25996  cgrane3  25997  cgrane4  25998  cgrahl1  25999  cgrahl2  26000  cgracgr  26001  cgraswap  26003  cgracom  26005  cgratr  26006  cgrabtwn  26008  cgrahl  26009  sacgr  26013  acopyeu  26016  cgrg3col4  26025  tgasa1  26030  f1otrg  26042  f1otrge  26043  axeuclidlem  26133  axcontlem2  26136  umgrvad2edg  26383  usgredg2vlem2  26396  pthdepisspth  26923  wwlksnwwlksnonOLD  27138  clwwlkccatlem  27216  clwlkclwwlklem2  27227  wwlksext2clwwlkOLD  27308  clwlksf1clwwlkOLD  27344  3cycld  27456  eupth2lems  27516  eucrctshift  27521  frgr3vlem2  27554  n4cyclfrgr  27571  numclwwlk1lem2f1  27649  numclwwlk1lem2f1OLD  27654  numclwwlk2lem1  27680  numclwwlk2lem1OLD  27691  ubthlem3  28184  chirredlem1  29705  chirredlem3  29707  cdj1i  29748  xrge0infss  29974  omndmul2  30159  submarchi  30187  gsumle  30226  xrge0tsmsd  30232  suborng  30262  isarchiofld  30264  psgnfzto1stlem  30297  fzto1st1  30299  smatrcl  30309  1smat1  30317  submateq  30322  mdetpmtr1  30336  madjusmdetlem2  30341  fimaproj  30347  locfinreflem  30354  cmppcmp  30372  ordtrest2NEWlem  30415  ordtconnlem1  30417  lmdvg  30446  esumpcvgval  30587  esum2d  30602  sigapildsys  30672  ldgenpisyslem1  30673  fiunelros  30684  volmeas  30741  imambfm  30771  omssubadd  30809  carsggect  30827  carsgclctunlem3  30829  sgnmul  31052  signsply0  31077  signstres  31102  actfunsnf1o  31133  actfunsnrndisj  31134  reprsuc  31144  reprinfz1  31151  breprexplema  31159  breprexplemc  31161  breprexp  31162  breprexpnat  31163  circlemeth  31169  hgt750lemb  31185  tgoldbachgtd  31191  erdszelem8  31628  pconnconn  31661  cvmlift2lem12  31744  cvmlift3lem5  31753  cvmlift3lem7  31755  cvmlift3lem8  31756  mrsubrn  31858  msrval  31883  msubff1  31901  slerec  32367  btwnconn1lem13  32650  elicc3  32755  neibastop2lem  32798  unbdqndv2  32941  ltflcei  33821  lindsenlbs  33828  matunitlindflem1  33829  matunitlindflem2  33830  poimirlem4  33837  poimirlem13  33846  poimirlem14  33847  poimirlem22  33855  poimirlem26  33859  poimirlem27  33860  heicant  33868  mblfinlem2  33871  mblfinlem3  33872  mblfinlem4  33873  cnambfre  33881  itg2addnclem  33884  itg2addnclem2  33885  itg2gt0cn  33888  bddiblnc  33903  ftc1cnnc  33907  ftc1anclem5  33912  ftc1anclem7  33914  ftc1anc  33916  equivtotbnd  33999  isbndx  34003  ssbnd  34009  heibor1lem  34030  rrncmslem  34053  islshpat  34973  lfl1dim  35077  lfl1dim2N  35078  lkrpssN  35119  glbconN  35333  hlhgt2  35345  3dim2  35424  3dim3  35425  islln3  35466  islvol5  35535  2lplnja  35575  dalem19  35638  isline4N  35733  2polssN  35871  lhpmatb  35987  4atex  36032  trlatn0  36128  cdlemf2  36518  dialss  37002  diaglbN  37011  diaintclN  37014  dibglbN  37122  dibintclN  37123  dihlsscpre  37190  dihglblem5aN  37248  dihglblem2aN  37249  dihglblem4  37253  dihatexv  37294  dihjat1lem  37384  lcfl6  37456  mapdval2N  37586  elrfi  37935  eldioph2  38003  diophin  38014  irrapxlem2  38065  irrapxlem3  38066  irrapxlem4  38067  irrapxlem5  38068  pell1234qrne0  38095  pell1234qrreccl  38096  pell1234qrmulcl  38097  pell14qrgt0  38101  pell14qrdich  38111  pell1qrge1  38112  pellfundex  38128  congabseq  38218  jm2.27b  38250  jm2.27  38252  fnwe2lem2  38298  kelac1  38310  lnrfg  38366  hbt  38377  cntzsdrg  38449  rfovcnvf1od  38972  ntrneiiso  39063  ntrneikb  39066  ntrneixb  39067  ntrneik3  39068  ntrneix3  39069  ntrneik13  39070  ntrneix13  39071  cvgdvgrat  39186  binomcxplemnotnn0  39229  sineq0ALT  39825  disjf1  40016  supxrgere  40187  supxrgelem  40191  supxrge  40192  suplesup  40193  xralrple2  40208  infxr  40221  infleinflem2  40225  infleinf  40226  uzub  40295  mccl  40468  limcrecl  40499  lptioo2  40501  lptioo1  40502  lptre2pt  40510  addlimc  40518  limsupmnflem  40590  climxrre  40620  liminflimsupclim  40677  climxlim2lem  40709  icccncfext  40738  cncfiooicclem1  40744  cncfiooiccre  40746  dvbdfbdioolem2  40782  ioodvbdlimc1lem1  40784  dvnxpaek  40795  dvmptfprodlem  40797  dvmptfprod  40798  dvnprodlem3  40801  itgioocnicc  40830  itgspltprt  40832  stoweidlem31  40885  fourierdlem39  41000  fourierdlem42  41003  fourierdlem48  41008  fourierdlem49  41009  fourierdlem50  41010  fourierdlem51  41011  fourierdlem64  41024  fourierdlem65  41025  fourierdlem74  41034  fourierdlem75  41035  fourierdlem81  41041  fourierdlem82  41042  fourierdlem101  41061  etransclem23  41111  etransclem27  41115  etransclem32  41120  etransclem33  41121  etransclem35  41123  etransclem38  41126  sge0tsms  41234  sge0cl  41235  sge0f1o  41236  sge0split  41263  sge0rpcpnf  41275  sge0seq  41300  nnfoctbdjlem  41309  iundjiun  41314  meaiuninc3v  41338  meaiininclem  41340  omeiunltfirp  41373  carageniuncllem2  41376  carageniuncl  41377  hoidmv1lelem1  41445  hoidmvlelem3  41451  hoidmvlelem5  41453  hoidmvle  41454  hoiqssbllem3  41478  iunhoiioolem  41529  pimdecfgtioo  41567  pimincfltioo  41568  preimageiingt  41570  preimaleiinlt  41571  smflimlem4  41622  iccpartigtl  42093  iccpartgt  42097  proththd  42207  sbgoldbst  42342  bgoldbtbndlem4  42372  sprsymrelf1lem  42410  resmgmhm2b  42469  2zrngmmgm  42615  cznrng  42624  rnghmsubcsetclem2  42645  rhmsubcsetclem2  42691  srhmsubc  42745  rhmsubclem4  42758  srhmsubcALTV  42763  rhmsubcALTVlem4  42776  lincsum  42887  lcoss  42894  snlindsntor  42929  islindeps2  42941