Theorem ad5antr 733

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 731	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 206  df-an 396

This theorem is referenced by:  ad6antr  735  ad6antlr  736  simp-5l  784  fimaproj  8134  catass  17659  catpropd  17682  cidpropd  17683  monpropd  17713  funcpropd  17882  fucpropd  17962  drsdirfi  18290  mhmmnd  19013  ghmquskerlem3  19230  neitr  23077  xkoccn  23516  trust  24127  restutopopn  24136  ucncn  24183  trcfilu  24192  ulmcau  26324  lgamucov  26963  tgcgrxfr  28315  tgbtwnconn1  28372  legov  28382  legso  28396  midexlem  28489  perpneq  28511  footexALT  28515  footex  28518  colperpexlem3  28529  colperpex  28530  opphllem  28532  opphllem3  28546  outpasch  28552  hlpasch  28553  lmieu  28581  trgcopy  28601  trgcopyeu  28603  dfcgra2  28627  acopyeu  28631  cgrg3col4  28650  f1otrg  28668  fnpreimac  32450  nn0xmulclb  32535  s3f1  32664  omndmul2  32786  cyc3conja  32872  isdrng4  32956  erler  32973  rlocf1  32981  fracfld  32988  dvdsruasso  33083  nsgqusf1olem3  33119  rhmquskerlem  33130  elrspunsn  33134  rhmimaidl  33137  mxidlprm  33173  ssmxidllem  33176  qsdrng  33198  fedgmul  33315  extdg1id  33341  qtophaus  33427  locfinreflem  33431  zarclssn  33464  hgt750lemb  34278  matunitlindflem1  37078  heicant  37117  mblfinlem3  37121  mblfinlem4  37122  itg2gt0cn  37137  sstotbnd2  37236  aks4d1p8  41547  aks6d1c2p2  41575  aks6d1c2  41585  aks6d1c6lem3  41628  fsuppind  41795  pell1234qrdich  42253  omabs2  42733  supxrgelem  44691  icccncfext  45247  etransclem35  45629  smflimlem2  46132