Theorem ad6antr 736

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 734	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  738  ad7antlr  739  simp-6l  786  catass  17609  funcpropd  17826  natpropd  17903  ghmqusnsg  19211  ghmquskerlem3  19215  rhmqusnsg  21240  restutop  24181  utopreg  24196  restmetu  24514  lgamucov  27004  istrkgcb  28528  tgifscgr  28580  tgbtwnconn1lem3  28646  legtrd  28661  miriso  28742  footexALT  28790  footex  28793  opphllem3  28821  opphl  28826  trgcopy  28876  cgratr  28895  dfcgra2  28902  inaghl  28917  cgrg3col4  28925  f1otrge  28944  clwlkclwwlklem2  30075  gsumwun  33158  cyc3genpm  33234  elrgspnlem4  33327  erler  33347  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rhmquskerlem  33506  elrspunidl  33509  rhmimaidl  33513  ssdifidllem  33537  ssdifidlprm  33539  mxidlirredi  33552  mxidlirred  33553  ssmxidllem  33554  qsdrngi  33576  1arithidom  33618  1arithufdlem3  33627  r1plmhm  33691  r1pquslmic  33692  lbsdiflsp0  33783  dimkerim  33784  fedgmul  33788  fldextrspunlsplem  33830  fldext2chn  33885  constrextdg2lem  33905  txomap  33991  matunitlindflem1  37817  heicant  37856  mblfinlem3  37860  primrootscoprmpow  42353  aks6d1c2lem4  42381  aks6d1c5  42393  limclner  45895  hoidmvle  46844  chnerlem1  47126