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  17647  funcpropd  17864  natpropd  17941  ghmqusnsg  19214  ghmquskerlem3  19218  rhmqusnsg  21195  restutop  24125  utopreg  24140  restmetu  24458  lgamucov  26948  istrkgcb  28383  tgifscgr  28435  tgbtwnconn1lem3  28501  legtrd  28516  miriso  28597  footexALT  28645  footex  28648  opphllem3  28676  opphl  28681  trgcopy  28731  cgratr  28750  dfcgra2  28757  inaghl  28772  cgrg3col4  28780  f1otrge  28799  clwlkclwwlklem2  29929  gsumwun  33005  cyc3genpm  33109  elrgspnlem4  33196  erler  33216  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rhmquskerlem  33396  elrspunidl  33399  rhmimaidl  33403  ssdifidllem  33427  ssdifidlprm  33429  mxidlirredi  33442  mxidlirred  33443  ssmxidllem  33444  qsdrngi  33466  1arithidom  33508  1arithufdlem3  33517  r1plmhm  33575  r1pquslmic  33576  lbsdiflsp0  33622  dimkerim  33623  fedgmul  33627  fldextrspunlsplem  33668  fldext2chn  33718  constrextdg2lem  33738  txomap  33824  matunitlindflem1  37610  heicant  37649  mblfinlem3  37653  primrootscoprmpow  42087  aks6d1c2lem4  42115  aks6d1c5  42127  limclner  45649  hoidmvle  46598