Theorem ad5antr 747

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad6antr  749  ad6antlr  750  simp-5l  797  fimaproj  8137  catass  17780  catpropd  17803  cidpropd  17804  monpropd  17832  funcpropd  17997  fucpropd  18075  drsdirfi  18399  chnind  18715  mhmmnd  19193  ghmqusnsg  19415  ghmquskerlem3  19419  omndmul2  20266  isdrng4  20908  rhmqusnsg  21494  ssdifidllem  21553  ssdifidlprm  21555  matunitlindflem1  22907  neitr  23411  xkoccn  23851  trust  24461  restutopopn  24470  ucncn  24516  trcfilu  24525  ulmcau  26638  lgamucov  27282  tgcgrxfr  28868  tgbtwnconn1  28925  legov  28935  legso  28949  tglnpt3  29009  tglnpt4  29010  midexlem  29051  perpneq  29076  footexALT  29080  footex  29083  colperpexlem3  29095  colperpex  29096  opphllem  29098  opphllem3  29112  outpasch  29120  hlpasch  29121  lnssplng  29157  lmieu  29176  trgcopy  29198  trgcopyeu  29200  dfcgra2  29225  acopyeu  29229  cgrarag  29231  tgaaddcpbl  29239  cgrg3col4  29259  angmgmaddeu1  29266  angmgmaddov2lem  29274  angmgmaddcpbl  29277  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlngmo2  29321  quadcgrprlng  29331  f1otrg  29335  fnpreimac  33151  nn0xmulclb  33250  s3f1  33398  ccatws1f1o  33401  mndlactf1o  33478  gsumwun  33524  gsumwrd2dccatlem  33525  cyc3conja  33605  elrgspnlem4  33693  erler  33713  rlocf1  33722  rlocisunit  33724  fracfld  33757  dvdsruasso  33826  nsgqusf1olem3  33852  rhmquskerlem  33861  elrspunsn  33865  rhmimaidl  33868  mxidlprm  33881  ssmxidllem  33884  qsdrng  33907  rprmasso2  33944  1arithufdlem3  33964  1arithufdlem4  33965  dfufd2lem  33967  mplvrpmrhm  34065  esplyfval1  34091  esplyind  34093  vieta  34098  fedgmul  34149  extdg1id  34184  constrextdg2lem  34266  qtophaus  34354  locfinreflem  34358  zarclssn  34391  hgt750lemb  35172  heicant  38412  mblfinlem3  38416  mblfinlem4  38417  itg2gt0cn  38432  sstotbnd2  38532  aks4d1p8  42961  aks6d1c2p2  42993  aks6d1c2  43004  aks6d1c6lem3  43046  unitscyglem3  43071  fsuppind  43444  pell1234qrdich  43710  omabs2  44181  supxrgelem  46175  icccncfext  46723  etransclem35  47105  smflimlem2  47608  uppropd  50115  fuco21  50270