Theorem ad5antr 740

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad6antr  742  ad6antlr  743  simp-5l  790  fimaproj  8082  catass  17650  catpropd  17673  cidpropd  17674  monpropd  17702  funcpropd  17867  fucpropd  17945  drsdirfi  18269  chnind  18585  mhmmnd  19038  ghmqusnsg  19255  ghmquskerlem3  19259  omndmul2  20106  rhmqusnsg  21285  neitr  23170  xkoccn  23609  trust  24219  restutopopn  24228  ucncn  24274  trcfilu  24283  ulmcau  26385  lgamucov  27026  tgcgrxfr  28611  tgbtwnconn1  28668  legov  28678  legso  28692  midexlem  28785  perpneq  28807  footexALT  28811  footex  28814  colperpexlem3  28825  colperpex  28826  opphllem  28828  opphllem3  28842  outpasch  28848  hlpasch  28849  lmieu  28877  trgcopy  28897  trgcopyeu  28899  dfcgra2  28923  acopyeu  28927  cgrg3col4  28946  f1otrg  28964  fnpreimac  32769  nn0xmulclb  32870  s3f1  33033  ccatws1f1o  33037  mndlactf1o  33116  gsumwun  33164  gsumwrd2dccatlem  33165  cyc3conja  33245  elrgspnlem4  33333  erler  33353  rlocf1  33361  isdrng4  33386  fracfld  33399  dvdsruasso  33475  nsgqusf1olem3  33505  rhmquskerlem  33515  elrspunsn  33519  rhmimaidl  33522  ssdifidllem  33546  ssdifidlprm  33548  mxidlprm  33560  ssmxidllem  33563  qsdrng  33587  rprmasso2  33616  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  mplvrpmrhm  33738  esplyfval1  33764  esplyind  33766  vieta  33771  fedgmul  33822  extdg1id  33857  constrextdg2lem  33939  qtophaus  34027  locfinreflem  34031  zarclssn  34064  hgt750lemb  34847  matunitlindflem1  37990  heicant  38029  mblfinlem3  38033  mblfinlem4  38034  itg2gt0cn  38049  sstotbnd2  38148  aks4d1p8  42579  aks6d1c2p2  42611  aks6d1c2  42622  aks6d1c6lem3  42664  unitscyglem3  42689  fsuppind  43047  pell1234qrdich  43313  omabs2  43784  supxrgelem  45789  icccncfext  46337  etransclem35  46719  smflimlem2  47222  uppropd  49678  fuco21  49833