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  8134  catass  17698  catpropd  17721  cidpropd  17722  monpropd  17750  funcpropd  17915  fucpropd  17993  drsdirfi  18317  mhmmnd  19047  ghmqusnsg  19265  ghmquskerlem3  19269  rhmqusnsg  21246  neitr  23118  xkoccn  23557  trust  24168  restutopopn  24177  ucncn  24223  trcfilu  24232  ulmcau  26356  lgamucov  27000  tgcgrxfr  28497  tgbtwnconn1  28554  legov  28564  legso  28578  midexlem  28671  perpneq  28693  footexALT  28697  footex  28700  colperpexlem3  28711  colperpex  28712  opphllem  28714  opphllem3  28728  outpasch  28734  hlpasch  28735  lmieu  28763  trgcopy  28783  trgcopyeu  28785  dfcgra2  28809  acopyeu  28813  cgrg3col4  28832  f1otrg  28850  fnpreimac  32649  nn0xmulclb  32748  s3f1  32922  ccatws1f1o  32927  chnind  32991  mndlactf1o  33025  gsumwun  33059  gsumwrd2dccatlem  33060  omndmul2  33080  cyc3conja  33168  elrgspnlem4  33240  erler  33260  rlocf1  33268  isdrng4  33289  fracfld  33302  dvdsruasso  33400  nsgqusf1olem3  33430  rhmquskerlem  33440  elrspunsn  33444  rhmimaidl  33447  ssdifidllem  33471  ssdifidlprm  33473  mxidlprm  33485  ssmxidllem  33488  qsdrng  33512  rprmasso2  33541  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  fedgmul  33671  extdg1id  33707  constrextdg2lem  33782  qtophaus  33867  locfinreflem  33871  zarclssn  33904  hgt750lemb  34688  matunitlindflem1  37640  heicant  37679  mblfinlem3  37683  mblfinlem4  37684  itg2gt0cn  37699  sstotbnd2  37798  aks4d1p8  42100  aks6d1c2p2  42132  aks6d1c2  42143  aks6d1c6lem3  42185  unitscyglem3  42210  fsuppind  42613  pell1234qrdich  42884  omabs2  43356  supxrgelem  45364  icccncfext  45916  etransclem35  46298  smflimlem2  46801  fuco21  49247