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  8065  catass  17589  catpropd  17612  cidpropd  17613  monpropd  17641  funcpropd  17806  fucpropd  17884  drsdirfi  18208  chnind  18524  mhmmnd  18974  ghmqusnsg  19192  ghmquskerlem3  19196  omndmul2  20043  rhmqusnsg  21220  neitr  23093  xkoccn  23532  trust  24142  restutopopn  24151  ucncn  24197  trcfilu  24206  ulmcau  26329  lgamucov  26973  tgcgrxfr  28494  tgbtwnconn1  28551  legov  28561  legso  28575  midexlem  28668  perpneq  28690  footexALT  28694  footex  28697  colperpexlem3  28708  colperpex  28709  opphllem  28711  opphllem3  28725  outpasch  28731  hlpasch  28732  lmieu  28760  trgcopy  28780  trgcopyeu  28782  dfcgra2  28806  acopyeu  28810  cgrg3col4  28829  f1otrg  28847  fnpreimac  32648  nn0xmulclb  32749  s3f1  32923  ccatws1f1o  32927  mndlactf1o  33006  gsumwun  33040  gsumwrd2dccatlem  33041  cyc3conja  33121  elrgspnlem4  33207  erler  33227  rlocf1  33235  isdrng4  33256  fracfld  33269  dvdsruasso  33345  nsgqusf1olem3  33375  rhmquskerlem  33385  elrspunsn  33389  rhmimaidl  33392  ssdifidllem  33416  ssdifidlprm  33418  mxidlprm  33430  ssmxidllem  33433  qsdrng  33457  rprmasso2  33486  1arithufdlem3  33506  1arithufdlem4  33507  dfufd2lem  33509  mplvrpmrhm  33572  fedgmul  33639  extdg1id  33674  constrextdg2lem  33756  qtophaus  33844  locfinreflem  33848  zarclssn  33881  hgt750lemb  34664  matunitlindflem1  37655  heicant  37694  mblfinlem3  37698  mblfinlem4  37699  itg2gt0cn  37714  sstotbnd2  37813  aks4d1p8  42119  aks6d1c2p2  42151  aks6d1c2  42162  aks6d1c6lem3  42204  unitscyglem3  42229  fsuppind  42622  pell1234qrdich  42893  omabs2  43364  supxrgelem  45375  icccncfext  45924  etransclem35  46306  smflimlem2  46809  uppropd  49212  fuco21  49367