Theorem ad5antr 734

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 732	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  736  ad6antlr  737  simp-5l  784  fimaproj  8117  catass  17654  catpropd  17677  cidpropd  17678  monpropd  17706  funcpropd  17871  fucpropd  17949  drsdirfi  18273  mhmmnd  19003  ghmqusnsg  19221  ghmquskerlem3  19225  rhmqusnsg  21202  neitr  23074  xkoccn  23513  trust  24124  restutopopn  24133  ucncn  24179  trcfilu  24188  ulmcau  26311  lgamucov  26955  tgcgrxfr  28452  tgbtwnconn1  28509  legov  28519  legso  28533  midexlem  28626  perpneq  28648  footexALT  28652  footex  28655  colperpexlem3  28666  colperpex  28667  opphllem  28669  opphllem3  28683  outpasch  28689  hlpasch  28690  lmieu  28718  trgcopy  28738  trgcopyeu  28740  dfcgra2  28764  acopyeu  28768  cgrg3col4  28787  f1otrg  28805  fnpreimac  32602  nn0xmulclb  32701  s3f1  32875  ccatws1f1o  32880  chnind  32944  mndlactf1o  32978  gsumwun  33012  gsumwrd2dccatlem  33013  omndmul2  33033  cyc3conja  33121  elrgspnlem4  33203  erler  33223  rlocf1  33231  isdrng4  33252  fracfld  33265  dvdsruasso  33363  nsgqusf1olem3  33393  rhmquskerlem  33403  elrspunsn  33407  rhmimaidl  33410  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  ssmxidllem  33451  qsdrng  33475  rprmasso2  33504  1arithufdlem3  33524  1arithufdlem4  33525  dfufd2lem  33527  fedgmul  33634  extdg1id  33668  constrextdg2lem  33745  qtophaus  33833  locfinreflem  33837  zarclssn  33870  hgt750lemb  34654  matunitlindflem1  37617  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  itg2gt0cn  37676  sstotbnd2  37775  aks4d1p8  42082  aks6d1c2p2  42114  aks6d1c2  42125  aks6d1c6lem3  42167  unitscyglem3  42192  fsuppind  42585  pell1234qrdich  42856  omabs2  43328  supxrgelem  45340  icccncfext  45892  etransclem35  46274  smflimlem2  46777  uppropd  49174  fuco21  49329