Theorem ad5antr 746

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 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 744	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad6antr  748  ad6antlr  749  simp-5l  796  fimaproj  8132  catass  17743  catpropd  17766  cidpropd  17767  monpropd  17795  funcpropd  17960  fucpropd  18038  drsdirfi  18362  chnind  18678  mhmmnd  19131  ghmqusnsg  19353  ghmquskerlem3  19357  omndmul2  20204  isdrng4  20826  rhmqusnsg  21406  ssdifidllem  21465  ssdifidlprm  21467  neitr  23318  xkoccn  23757  trust  24367  restutopopn  24376  ucncn  24422  trcfilu  24431  ulmcau  26539  lgamucov  27183  tgcgrxfr  28768  tgbtwnconn1  28825  legov  28835  legso  28849  tglnpt3  28908  tglnpt4  28909  midexlem  28950  perpneq  28975  footexALT  28979  footex  28982  colperpexlem3  28994  colperpex  28995  opphllem  28997  opphllem3  29011  outpasch  29018  hlpasch  29019  lnssplng  29055  lmieu  29074  trgcopy  29096  trgcopyeu  29098  dfcgra2  29122  acopyeu  29126  cgrarag  29128  cgrg3col4  29151  perpprlng  29181  prlngex  29182  prlngmolem1  29183  prlngmolem2  29184  prlngmo2  29187  quadcgrprlng  29197  f1otrg  29201  fnpreimac  32996  nn0xmulclb  33097  s3f1  33248  ccatws1f1o  33252  mndlactf1o  33331  gsumwun  33377  gsumwrd2dccatlem  33378  cyc3conja  33458  elrgspnlem4  33546  erler  33566  rlocf1  33575  rlocisunit  33577  fracfld  33610  dvdsruasso  33679  nsgqusf1olem3  33705  rhmquskerlem  33714  elrspunsn  33718  rhmimaidl  33721  mxidlprm  33734  ssmxidllem  33737  qsdrng  33760  rprmasso2  33797  1arithufdlem3  33817  1arithufdlem4  33818  dfufd2lem  33820  mplvrpmrhm  33918  esplyfval1  33944  esplyind  33946  vieta  33951  fedgmul  34002  extdg1id  34037  constrextdg2lem  34119  qtophaus  34207  locfinreflem  34211  zarclssn  34244  hgt750lemb  35024  matunitlindflem1  38248  heicant  38287  mblfinlem3  38291  mblfinlem4  38292  itg2gt0cn  38307  sstotbnd2  38406  aks4d1p8  42835  aks6d1c2p2  42867  aks6d1c2  42878  aks6d1c6lem3  42920  unitscyglem3  42945  fsuppind  43305  pell1234qrdich  43571  omabs2  44042  supxrgelem  46036  icccncfext  46584  etransclem35  46966  smflimlem2  47469  uppropd  49942  fuco21  50097