Theorem ad5antr 735

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad6antr  737  ad6antlr  738  simp-5l  785  fimaproj  8085  catass  17652  catpropd  17675  cidpropd  17676  monpropd  17704  funcpropd  17869  fucpropd  17947  drsdirfi  18271  chnind  18587  mhmmnd  19040  ghmqusnsg  19257  ghmquskerlem3  19261  omndmul2  20108  rhmqusnsg  21283  neitr  23145  xkoccn  23584  trust  24194  restutopopn  24203  ucncn  24249  trcfilu  24258  ulmcau  26360  lgamucov  27001  tgcgrxfr  28586  tgbtwnconn1  28643  legov  28653  legso  28667  midexlem  28760  perpneq  28782  footexALT  28786  footex  28789  colperpexlem3  28800  colperpex  28801  opphllem  28803  opphllem3  28817  outpasch  28823  hlpasch  28824  lmieu  28852  trgcopy  28872  trgcopyeu  28874  dfcgra2  28898  acopyeu  28902  cgrg3col4  28921  f1otrg  28939  fnpreimac  32743  nn0xmulclb  32844  s3f1  33007  ccatws1f1o  33011  mndlactf1o  33090  gsumwun  33137  gsumwrd2dccatlem  33138  cyc3conja  33218  elrgspnlem4  33306  erler  33326  rlocf1  33334  isdrng4  33356  fracfld  33369  dvdsruasso  33445  nsgqusf1olem3  33475  rhmquskerlem  33485  elrspunsn  33489  rhmimaidl  33492  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  ssmxidllem  33533  qsdrng  33557  rprmasso2  33586  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  mplvrpmrhm  33691  esplyfval1  33717  esplyind  33719  vieta  33724  fedgmul  33775  extdg1id  33810  constrextdg2lem  33892  qtophaus  33980  locfinreflem  33984  zarclssn  34017  hgt750lemb  34800  matunitlindflem1  37937  heicant  37976  mblfinlem3  37980  mblfinlem4  37981  itg2gt0cn  37996  sstotbnd2  38095  aks4d1p8  42526  aks6d1c2p2  42558  aks6d1c2  42569  aks6d1c6lem3  42611  unitscyglem3  42636  fsuppind  43023  pell1234qrdich  43289  omabs2  43760  supxrgelem  45767  icccncfext  46315  etransclem35  46697  smflimlem2  47200  uppropd  49656  fuco21  49811