Theorem ad4antr 733

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad4antr	⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 731	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:  ad5antr  735  ad5antlr  736  simp-4l  783  tfrlem1  8317  prdsval  17387  catass  17621  catpropd  17644  cidpropd  17645  subccocl  17781  funcco  17807  natpropd  17915  fucpropd  17916  initoeu2lem1  17950  prfval  18134  xpcpropd  18143  acsfiindd  18488  chnind  18556  chnso  18559  mndpsuppss  18702  mhmmnd  19006  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  omndmul2  20074  rhmpreimaidl  21244  rhmqusnsg  21252  mhpmulcl  22104  psdmul  22121  scmatscm  22469  cpmatmcllem  22674  mptcoe1matfsupp  22758  mp2pm2mplem4  22765  chpdmatlem2  22795  chfacfisf  22810  chfacfisfcpmat  22811  neitr  23136  hauscmplem  23362  trcfilu  24249  cfilucfil  24515  restmetu  24526  metucn  24527  cnheibor  24922  dvlip2  25968  lgamucov  27016  bdayfinbndlem1  28475  tgifscgr  28592  iscgrglt  28598  tgbtwnconn1  28659  legtrd  28673  legtri3  28674  legso  28683  hlcgrex  28700  tglndim0  28713  tglinethru  28720  tglnpt2  28725  colline  28733  perpneq  28798  isperp2  28799  footexALT  28802  opphllem  28819  midex  28821  opphllem3  28833  opphllem5  28835  opphllem6  28836  opphl  28838  outpasch  28839  hlpasch  28840  lnopp2hpgb  28847  hpgerlem  28849  lmieu  28868  lnperpex  28887  trgcopy  28888  cgrahl  28911  acopy  28917  inaghl  28929  cgrg3col4  28937  f1otrg  28955  nbumgrvtx  29431  3cyclfrgr  30375  numclwlk2lem2f1o  30466  s3f1  33039  ccatws1f1o  33043  dfmgc2  33088  pwrssmgc  33092  mgcf1o  33095  mndlrinvb  33117  gsumwun  33169  psgnfzto1stlem  33193  cycpmrn  33236  tocyccntz  33237  cycpmconjs  33249  isarchi3  33280  archirngz  33282  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem2  33341  erler  33358  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rloc1r  33365  fracfld  33401  nsgqusf1olem1  33505  nsgqusf1olem2  33506  nsgqusf1olem3  33507  lmhmqusker  33509  rhmquskerlem  33517  elrspunidl  33520  elrspunsn  33521  idlinsubrg  33523  rhmimaidl  33524  drngidl  33525  isprmidlc  33539  qsidomlem1  33544  qsidomlem2  33545  ssdifidlprm  33550  mxidlprm  33562  mxidlirredi  33563  mxidlirred  33564  drngmxidlr  33570  opprqusplusg  33581  opprqusmulr  33583  qsdrngi  33587  qsdrng  33589  rsprprmprmidlb  33615  rprmirred  33623  rprmirredb  33624  rprmdvdsprod  33626  1arithidom  33629  pidufd  33635  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  dfufd2lem  33641  deg1prod  33675  mplmulmvr  33715  mplvrpmrhm  33723  psrgsum  33724  psrmonprod  33728  esplyfv  33746  esplyfval1  33749  esplyind  33751  dimkerim  33804  fedgmul  33808  extdg1id  33843  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem1  33869  extdgfialg  33871  minplyirred  33888  constrextdg2lem  33925  constrfiss  33928  cos9thpiminplylem2  33960  qtophaus  34013  zarclsint  34049  zarcmplem  34058  esumcst  34240  sigapildsys  34339  oms0  34474  omssubadd  34477  carsgclctunlem3  34497  eulerpartlemgvv  34553  signsply0  34728  signstfvneq0  34749  actfunsnf1o  34781  reprsuc  34792  reprinfz1  34799  breprexplema  34807  breprexplemc  34809  hgt750lemb  34833  cvmlift3lem2  35533  satfdmlem  35581  nn0prpwlem  36535  lindsenlbs  37863  matunitlindflem1  37864  mblfinlem3  37907  mblfinlem4  37908  itg2addnclem2  37920  itg2gt0cn  37923  ftc1cnnc  37940  ftc1anc  37949  sstotbnd2  38022  lcfl8  41875  aks4d1p8  42454  fldhmf1  42457  mndmolinv  42462  primrootsunit1  42464  primrootscoprmpow  42466  primrootspoweq0  42473  aks6d1c2p2  42486  aks6d1c2lem4  42494  aks6d1c6lem3  42539  aks6d1c7  42551  unitscyglem2  42563  aks5  42571  fiabv  42903  fsuppind  42945  prjspersym  42962  pell1234qrdich  43215  pell14qrdich  43223  pell1qrgap  43228  pellfundex  43240  omabs2  43686  cvgdvgrat  44666  infleinflem2  45726  xrralrecnnle  45738  climrec  45960  climsuse  45965  limcrecl  45986  limsupubuz  46068  limsupgtlem  46132  xlimliminflimsup  46217  fperdvper  46274  dvnprodlem2  46302  etransclem35  46624  hspmbllem2  46982  smflimlem2  47127  smflimlem4  47129  iccpartgt  47784  prproropf1olem4  47863  sfprmdvdsmersenne  47960  gricushgr  48274  2zlidl  48597  ply1mulgsumlem2  48744  nn0sumshdiglemA  48976  imaf1co  49511  uppropd  49537  fuco21  49692  functhinclem4  49803  2arwcat  49956