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  8140  catass  17767  catpropd  17790  cidpropd  17791  monpropd  17819  funcpropd  17984  fucpropd  18062  drsdirfi  18386  chnind  18702  mhmmnd  19155  ghmqusnsg  19377  ghmquskerlem3  19381  omndmul2  20228  isdrng4  20869  rhmqusnsg  21455  ssdifidllem  21514  ssdifidlprm  21516  neitr  23367  xkoccn  23806  trust  24416  restutopopn  24425  ucncn  24471  trcfilu  24480  ulmcau  26588  lgamucov  27232  tgcgrxfr  28817  tgbtwnconn1  28874  legov  28884  legso  28898  tglnpt3  28957  tglnpt4  28958  midexlem  28999  perpneq  29024  footexALT  29028  footex  29031  colperpexlem3  29043  colperpex  29044  opphllem  29046  opphllem3  29060  outpasch  29067  hlpasch  29068  lnssplng  29104  lmieu  29123  trgcopy  29145  trgcopyeu  29147  dfcgra2  29171  acopyeu  29175  cgrarag  29177  cgrg3col4  29200  perpprlng  29230  prlngex  29231  prlngmolem1  29232  prlngmolem2  29233  prlngmo2  29236  quadcgrprlng  29246  f1otrg  29250  fnpreimac  33045  nn0xmulclb  33146  s3f1  33294  ccatws1f1o  33297  mndlactf1o  33374  gsumwun  33420  gsumwrd2dccatlem  33421  cyc3conja  33501  elrgspnlem4  33589  erler  33609  rlocf1  33618  rlocisunit  33620  fracfld  33653  dvdsruasso  33722  nsgqusf1olem3  33748  rhmquskerlem  33757  elrspunsn  33761  rhmimaidl  33764  mxidlprm  33777  ssmxidllem  33780  qsdrng  33803  rprmasso2  33840  1arithufdlem3  33860  1arithufdlem4  33861  dfufd2lem  33863  mplvrpmrhm  33961  esplyfval1  33987  esplyind  33989  vieta  33994  fedgmul  34045  extdg1id  34080  constrextdg2lem  34162  qtophaus  34250  locfinreflem  34254  zarclssn  34287  hgt750lemb  35067  matunitlindflem1  38300  heicant  38339  mblfinlem3  38343  mblfinlem4  38344  itg2gt0cn  38359  sstotbnd2  38458  aks4d1p8  42887  aks6d1c2p2  42919  aks6d1c2  42930  aks6d1c6lem3  42972  unitscyglem3  42997  fsuppind  43355  pell1234qrdich  43621  omabs2  44092  supxrgelem  46086  icccncfext  46634  etransclem35  47016  smflimlem2  47519  uppropd  49992  fuco21  50147