Theorem ad5antr 744

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad6antr  746  ad6antlr  747  simp-5l  794  fimaproj  8110  catass  17701  catpropd  17724  cidpropd  17725  monpropd  17753  funcpropd  17918  fucpropd  17996  drsdirfi  18320  chnind  18636  mhmmnd  19089  ghmqusnsg  19305  ghmquskerlem3  19309  omndmul2  20156  rhmqusnsg  21335  neitr  23220  xkoccn  23659  trust  24269  restutopopn  24278  ucncn  24324  trcfilu  24333  ulmcau  26435  lgamucov  27079  tgcgrxfr  28664  tgbtwnconn1  28721  legov  28731  legso  28745  midexlem  28838  perpneq  28860  footexALT  28864  footex  28867  colperpexlem3  28878  colperpex  28879  opphllem  28881  opphllem3  28895  outpasch  28901  hlpasch  28902  lmieu  28930  trgcopy  28950  trgcopyeu  28952  dfcgra2  28976  acopyeu  28980  cgrg3col4  28999  f1otrg  29017  fnpreimac  32822  nn0xmulclb  32923  s3f1  33086  ccatws1f1o  33090  mndlactf1o  33169  gsumwun  33217  gsumwrd2dccatlem  33218  cyc3conja  33298  elrgspnlem4  33387  erler  33407  rlocf1  33416  rlocisunit  33418  isdrng4  33443  fracfld  33456  dvdsruasso  33532  nsgqusf1olem3  33562  rhmquskerlem  33572  elrspunsn  33576  rhmimaidl  33579  ssdifidllem  33604  ssdifidlprm  33606  mxidlprm  33619  ssmxidllem  33622  qsdrng  33646  rprmasso2  33683  1arithufdlem3  33703  1arithufdlem4  33704  dfufd2lem  33706  mplvrpmrhm  33805  esplyfval1  33831  esplyind  33833  vieta  33838  fedgmul  33889  extdg1id  33924  constrextdg2lem  34006  qtophaus  34094  locfinreflem  34098  zarclssn  34131  hgt750lemb  34914  matunitlindflem1  38079  heicant  38118  mblfinlem3  38122  mblfinlem4  38123  itg2gt0cn  38138  sstotbnd2  38237  aks4d1p8  42668  aks6d1c2p2  42700  aks6d1c2  42711  aks6d1c6lem3  42753  unitscyglem3  42778  fsuppind  43136  pell1234qrdich  43402  omabs2  43873  supxrgelem  45877  icccncfext  46425  etransclem35  46807  smflimlem2  47310  uppropd  49766  fuco21  49921