Theorem ad6antr 737

Description: Deduction adding 6 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
ad6antr	⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 735	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:  ad7antr  739  ad7antlr  740  simp-6l  787  catass  17652  funcpropd  17869  natpropd  17946  ghmqusnsg  19257  ghmquskerlem3  19261  rhmqusnsg  21283  restutop  24202  utopreg  24217  restmetu  24535  lgamucov  27001  istrkgcb  28524  tgifscgr  28576  tgbtwnconn1lem3  28642  legtrd  28657  miriso  28738  footexALT  28786  footex  28789  opphllem3  28817  opphl  28822  trgcopy  28872  cgratr  28891  dfcgra2  28898  inaghl  28913  cgrg3col4  28921  f1otrge  28940  clwlkclwwlklem2  30070  gsumwun  33137  cyc3genpm  33213  elrgspnlem4  33306  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rhmquskerlem  33485  elrspunidl  33488  rhmimaidl  33492  ssdifidllem  33516  ssdifidlprm  33518  mxidlirredi  33531  mxidlirred  33532  ssmxidllem  33533  qsdrngi  33555  1arithidom  33597  1arithufdlem3  33606  r1plmhm  33670  r1pquslmic  33671  lbsdiflsp0  33770  dimkerim  33771  fedgmul  33775  fldextrspunlsplem  33817  fldext2chn  33872  constrextdg2lem  33892  txomap  33978  matunitlindflem1  37937  heicant  37976  mblfinlem3  37980  primrootscoprmpow  42538  aks6d1c2lem4  42566  aks6d1c5  42578  limclner  46079  hoidmvle  47028  chnerlem1  47312