Theorem ad5antr 734

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 732	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  736  ad6antlr  737  simp-5l  784  fimaproj  8071  catass  17594  catpropd  17617  cidpropd  17618  monpropd  17646  funcpropd  17811  fucpropd  17889  drsdirfi  18213  chnind  18529  mhmmnd  18979  ghmqusnsg  19196  ghmquskerlem3  19200  omndmul2  20047  rhmqusnsg  21224  neitr  23096  xkoccn  23535  trust  24145  restutopopn  24154  ucncn  24200  trcfilu  24209  ulmcau  26332  lgamucov  26976  tgcgrxfr  28497  tgbtwnconn1  28554  legov  28564  legso  28578  midexlem  28671  perpneq  28693  footexALT  28697  footex  28700  colperpexlem3  28711  colperpex  28712  opphllem  28714  opphllem3  28728  outpasch  28734  hlpasch  28735  lmieu  28763  trgcopy  28783  trgcopyeu  28785  dfcgra2  28809  acopyeu  28813  cgrg3col4  28832  f1otrg  28850  fnpreimac  32655  nn0xmulclb  32758  s3f1  32935  ccatws1f1o  32939  mndlactf1o  33018  gsumwun  33052  gsumwrd2dccatlem  33053  cyc3conja  33133  elrgspnlem4  33219  erler  33239  rlocf1  33247  isdrng4  33268  fracfld  33281  dvdsruasso  33357  nsgqusf1olem3  33387  rhmquskerlem  33397  elrspunsn  33401  rhmimaidl  33404  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  ssmxidllem  33445  qsdrng  33469  rprmasso2  33498  1arithufdlem3  33518  1arithufdlem4  33519  dfufd2lem  33521  mplvrpmrhm  33595  esplyind  33613  fedgmul  33665  extdg1id  33700  constrextdg2lem  33782  qtophaus  33870  locfinreflem  33874  zarclssn  33907  hgt750lemb  34690  matunitlindflem1  37676  heicant  37715  mblfinlem3  37719  mblfinlem4  37720  itg2gt0cn  37735  sstotbnd2  37834  aks4d1p8  42200  aks6d1c2p2  42232  aks6d1c2  42243  aks6d1c6lem3  42285  unitscyglem3  42310  fsuppind  42708  pell1234qrdich  42978  omabs2  43449  supxrgelem  45460  icccncfext  46009  etransclem35  46391  smflimlem2  46894  uppropd  49306  fuco21  49461