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  8154  catass  17865  catpropd  17888  cidpropd  17889  monpropd  17917  funcpropd  18082  fucpropd  18160  drsdirfi  18484  chnind  18800  mhmmnd  19279  ghmqusnsg  19501  ghmquskerlem3  19505  omndmul2  20352  isdrng4  20997  rhmqusnsg  21586  ssdifidllem  21645  ssdifidlprm  21647  matunitlindflem1  22999  neitr  23503  xkoccn  23943  trust  24553  restutopopn  24562  ucncn  24608  trcfilu  24617  ulmcau  26727  lgamucov  27370  tgcgrxfr  28986  tgbtwnconn1  29043  legov  29053  legso  29067  tglnpt3  29127  tglnpt4  29128  midexlem  29169  perpneq  29194  footexALT  29198  footex  29201  colperpexlem3  29213  colperpex  29214  opphllem  29216  opphllem3  29230  outpasch  29238  hlpasch  29239  lnssplng  29275  lmieu  29294  trgcopy  29316  trgcopyeu  29318  dfcgra2  29343  acopyeu  29347  cgrarag  29349  tgaaddcpbl  29357  cgrg3col4  29377  angmgmaddeu1  29384  angmgmaddov2lem  29392  angmgmaddcpbl  29395  perpprlng  29433  prlngex  29434  prlngmolem1  29435  prlngmolem2  29436  prlngmo2  29439  quadcgrprlng  29449  f1otrg  29453  fnpreimac  33311  nn0xmulclb  33409  s3f1  33557  ccatws1f1o  33560  mndlactf1o  33637  gsumwun  33683  gsumwrd2dccatlem  33684  cyc3conja  33764  elrgspnlem4  33852  erler  33872  rlocf1  33881  rlocisunit  33883  fracfld  33916  dvdsruasso  33986  nsgqusf1olem3  34012  rhmquskerlem  34021  elrspunsn  34025  rhmimaidl  34028  mxidlprm  34041  ssmxidllem  34044  qsdrng  34067  rprmasso2  34104  1arithufdlem3  34124  1arithufdlem4  34125  dfufd2lem  34127  mplvrpmrhm  34225  esplyfval1  34251  esplyind  34253  vieta  34258  fedgmul  34309  extdg1id  34344  constrextdg2lem  34426  qtophaus  34514  locfinreflem  34518  zarclssn  34551  hgt750lemb  35331  heicant  38666  mblfinlem3  38670  mblfinlem4  38671  itg2gt0cn  38686  sstotbnd2  38801  aks4d1p8  43230  aks6d1c2p2  43262  aks6d1c2  43273  aks6d1c6lem3  43315  unitscyglem3  43340  fsuppind  43711  pell1234qrdich  43961  omabs2  44427  supxrgelem  46442  icccncfext  46990  etransclem35  47372  smflimlem2  47875  uppropd  50390  fuco21  50551