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  19161  ghmqusnsg  19383  ghmquskerlem3  19387  omndmul2  20234  isdrng4  20876  rhmqusnsg  21462  ssdifidllem  21521  ssdifidlprm  21523  neitr  23374  xkoccn  23813  trust  24423  restutopopn  24432  ucncn  24478  trcfilu  24487  ulmcau  26595  lgamucov  27239  tgcgrxfr  28824  tgbtwnconn1  28881  legov  28891  legso  28905  tglnpt3  28964  tglnpt4  28965  midexlem  29006  perpneq  29031  footexALT  29035  footex  29038  colperpexlem3  29050  colperpex  29051  opphllem  29053  opphllem3  29067  outpasch  29074  hlpasch  29075  lnssplng  29111  lmieu  29130  trgcopy  29152  trgcopyeu  29154  dfcgra2  29178  acopyeu  29182  cgrarag  29184  cgrg3col4  29207  perpprlng  29237  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  prlngmo2  29243  quadcgrprlng  29253  f1otrg  29257  fnpreimac  33052  nn0xmulclb  33153  s3f1  33301  ccatws1f1o  33304  mndlactf1o  33381  gsumwun  33427  gsumwrd2dccatlem  33428  cyc3conja  33508  elrgspnlem4  33596  erler  33616  rlocf1  33625  rlocisunit  33627  fracfld  33660  dvdsruasso  33729  nsgqusf1olem3  33755  rhmquskerlem  33764  elrspunsn  33768  rhmimaidl  33771  mxidlprm  33784  ssmxidllem  33787  qsdrng  33810  rprmasso2  33847  1arithufdlem3  33867  1arithufdlem4  33868  dfufd2lem  33870  mplvrpmrhm  33968  esplyfval1  33994  esplyind  33996  vieta  34001  fedgmul  34052  extdg1id  34087  constrextdg2lem  34169  qtophaus  34257  locfinreflem  34261  zarclssn  34294  hgt750lemb  35075  matunitlindflem1  38308  heicant  38347  mblfinlem3  38351  mblfinlem4  38352  itg2gt0cn  38367  sstotbnd2  38466  aks4d1p8  42895  aks6d1c2p2  42927  aks6d1c2  42938  aks6d1c6lem3  42980  unitscyglem3  43005  fsuppind  43363  pell1234qrdich  43629  omabs2  44100  supxrgelem  46094  icccncfext  46642  etransclem35  47024  smflimlem2  47527  uppropd  50000  fuco21  50155