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  785  fimaproj  8158  catass  17730  catpropd  17753  cidpropd  17754  monpropd  17784  funcpropd  17953  fucpropd  18033  drsdirfi  18362  mhmmnd  19094  ghmqusnsg  19312  ghmquskerlem3  19316  rhmqusnsg  21312  neitr  23203  xkoccn  23642  trust  24253  restutopopn  24262  ucncn  24309  trcfilu  24318  ulmcau  26452  lgamucov  27095  tgcgrxfr  28540  tgbtwnconn1  28597  legov  28607  legso  28621  midexlem  28714  perpneq  28736  footexALT  28740  footex  28743  colperpexlem3  28754  colperpex  28755  opphllem  28757  opphllem3  28771  outpasch  28777  hlpasch  28778  lmieu  28806  trgcopy  28826  trgcopyeu  28828  dfcgra2  28852  acopyeu  28856  cgrg3col4  28875  f1otrg  28893  fnpreimac  32687  nn0xmulclb  32781  s3f1  32915  ccatws1f1o  32920  chnind  32984  mndlactf1o  33017  gsumwun  33050  gsumwrd2dccatlem  33051  omndmul2  33071  cyc3conja  33159  elrgspnlem4  33234  erler  33251  rlocf1  33259  isdrng4  33278  fracfld  33289  dvdsruasso  33392  nsgqusf1olem3  33422  rhmquskerlem  33432  elrspunsn  33436  rhmimaidl  33439  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  ssmxidllem  33480  qsdrng  33504  rprmasso2  33533  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  fedgmul  33658  extdg1id  33690  qtophaus  33796  locfinreflem  33800  zarclssn  33833  hgt750lemb  34649  matunitlindflem1  37602  heicant  37641  mblfinlem3  37645  mblfinlem4  37646  itg2gt0cn  37661  sstotbnd2  37760  aks4d1p8  42068  aks6d1c2p2  42100  aks6d1c2  42111  aks6d1c6lem3  42153  unitscyglem3  42178  fsuppind  42576  pell1234qrdich  42848  omabs2  43321  supxrgelem  45286  icccncfext  45842  etransclem35  46224  smflimlem2  46727