Theorem ad5antr 735

Description: Deduction adding 5 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
ad5antr	⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 733	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:  ad6antr  737  ad6antlr  738  simp-5l  785  fimaproj  8087  catass  17621  catpropd  17644  cidpropd  17645  monpropd  17673  funcpropd  17838  fucpropd  17916  drsdirfi  18240  chnind  18556  mhmmnd  19006  ghmqusnsg  19223  ghmquskerlem3  19227  omndmul2  20074  rhmqusnsg  21252  neitr  23136  xkoccn  23575  trust  24185  restutopopn  24194  ucncn  24240  trcfilu  24249  ulmcau  26372  lgamucov  27016  tgcgrxfr  28602  tgbtwnconn1  28659  legov  28669  legso  28683  midexlem  28776  perpneq  28798  footexALT  28802  footex  28805  colperpexlem3  28816  colperpex  28817  opphllem  28819  opphllem3  28833  outpasch  28839  hlpasch  28840  lmieu  28868  trgcopy  28888  trgcopyeu  28890  dfcgra2  28914  acopyeu  28918  cgrg3col4  28937  f1otrg  28955  fnpreimac  32759  nn0xmulclb  32861  s3f1  33039  ccatws1f1o  33043  mndlactf1o  33122  gsumwun  33169  gsumwrd2dccatlem  33170  cyc3conja  33250  elrgspnlem4  33338  erler  33358  rlocf1  33366  isdrng4  33388  fracfld  33401  dvdsruasso  33477  nsgqusf1olem3  33507  rhmquskerlem  33517  elrspunsn  33521  rhmimaidl  33524  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  ssmxidllem  33565  qsdrng  33589  rprmasso2  33618  1arithufdlem3  33638  1arithufdlem4  33639  dfufd2lem  33641  mplvrpmrhm  33723  esplyfval1  33749  esplyind  33751  vieta  33756  fedgmul  33808  extdg1id  33843  constrextdg2lem  33925  qtophaus  34013  locfinreflem  34017  zarclssn  34050  hgt750lemb  34833  matunitlindflem1  37861  heicant  37900  mblfinlem3  37904  mblfinlem4  37905  itg2gt0cn  37920  sstotbnd2  38019  aks4d1p8  42451  aks6d1c2p2  42483  aks6d1c2  42494  aks6d1c6lem3  42536  unitscyglem3  42561  fsuppind  42942  pell1234qrdich  43212  omabs2  43683  supxrgelem  45690  icccncfext  46239  etransclem35  46621  smflimlem2  47124  uppropd  49534  fuco21  49689