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  8077  catass  17609  catpropd  17632  cidpropd  17633  monpropd  17661  funcpropd  17826  fucpropd  17904  drsdirfi  18228  chnind  18544  mhmmnd  18994  ghmqusnsg  19211  ghmquskerlem3  19215  omndmul2  20062  rhmqusnsg  21240  neitr  23124  xkoccn  23563  trust  24173  restutopopn  24182  ucncn  24228  trcfilu  24237  ulmcau  26360  lgamucov  27004  tgcgrxfr  28590  tgbtwnconn1  28647  legov  28657  legso  28671  midexlem  28764  perpneq  28786  footexALT  28790  footex  28793  colperpexlem3  28804  colperpex  28805  opphllem  28807  opphllem3  28821  outpasch  28827  hlpasch  28828  lmieu  28856  trgcopy  28876  trgcopyeu  28878  dfcgra2  28902  acopyeu  28906  cgrg3col4  28925  f1otrg  28943  fnpreimac  32749  nn0xmulclb  32851  s3f1  33029  ccatws1f1o  33033  mndlactf1o  33112  gsumwun  33158  gsumwrd2dccatlem  33159  cyc3conja  33239  elrgspnlem4  33327  erler  33347  rlocf1  33355  isdrng4  33377  fracfld  33390  dvdsruasso  33466  nsgqusf1olem3  33496  rhmquskerlem  33506  elrspunsn  33510  rhmimaidl  33513  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  ssmxidllem  33554  qsdrng  33578  rprmasso2  33607  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  mplvrpmrhm  33712  esplyind  33731  vieta  33736  fedgmul  33788  extdg1id  33823  constrextdg2lem  33905  qtophaus  33993  locfinreflem  33997  zarclssn  34030  hgt750lemb  34813  matunitlindflem1  37813  heicant  37852  mblfinlem3  37856  mblfinlem4  37857  itg2gt0cn  37872  sstotbnd2  37971  aks4d1p8  42337  aks6d1c2p2  42369  aks6d1c2  42380  aks6d1c6lem3  42422  unitscyglem3  42447  fsuppind  42829  pell1234qrdich  43099  omabs2  43570  supxrgelem  45578  icccncfext  46127  etransclem35  46509  smflimlem2  47012  uppropd  49422  fuco21  49577