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  8114  catass  17647  catpropd  17670  cidpropd  17671  monpropd  17699  funcpropd  17864  fucpropd  17942  drsdirfi  18266  mhmmnd  18996  ghmqusnsg  19214  ghmquskerlem3  19218  rhmqusnsg  21195  neitr  23067  xkoccn  23506  trust  24117  restutopopn  24126  ucncn  24172  trcfilu  24181  ulmcau  26304  lgamucov  26948  tgcgrxfr  28445  tgbtwnconn1  28502  legov  28512  legso  28526  midexlem  28619  perpneq  28641  footexALT  28645  footex  28648  colperpexlem3  28659  colperpex  28660  opphllem  28662  opphllem3  28676  outpasch  28682  hlpasch  28683  lmieu  28711  trgcopy  28731  trgcopyeu  28733  dfcgra2  28757  acopyeu  28761  cgrg3col4  28780  f1otrg  28798  fnpreimac  32595  nn0xmulclb  32694  s3f1  32868  ccatws1f1o  32873  chnind  32937  mndlactf1o  32971  gsumwun  33005  gsumwrd2dccatlem  33006  omndmul2  33026  cyc3conja  33114  elrgspnlem4  33196  erler  33216  rlocf1  33224  isdrng4  33245  fracfld  33258  dvdsruasso  33356  nsgqusf1olem3  33386  rhmquskerlem  33396  elrspunsn  33400  rhmimaidl  33403  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  ssmxidllem  33444  qsdrng  33468  rprmasso2  33497  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  fedgmul  33627  extdg1id  33661  constrextdg2lem  33738  qtophaus  33826  locfinreflem  33830  zarclssn  33863  hgt750lemb  34647  matunitlindflem1  37610  heicant  37649  mblfinlem3  37653  mblfinlem4  37654  itg2gt0cn  37669  sstotbnd2  37768  aks4d1p8  42075  aks6d1c2p2  42107  aks6d1c2  42118  aks6d1c6lem3  42160  unitscyglem3  42185  fsuppind  42578  pell1234qrdich  42849  omabs2  43321  supxrgelem  45333  icccncfext  45885  etransclem35  46267  smflimlem2  46770  uppropd  49170  fuco21  49325