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  17613  funcpropd  17830  natpropd  17907  ghmqusnsg  19215  ghmquskerlem3  19219  rhmqusnsg  21244  restutop  24185  utopreg  24200  restmetu  24518  lgamucov  27008  istrkgcb  28511  tgifscgr  28563  tgbtwnconn1lem3  28629  legtrd  28644  miriso  28725  footexALT  28773  footex  28776  opphllem3  28804  opphl  28809  trgcopy  28859  cgratr  28878  dfcgra2  28885  inaghl  28900  cgrg3col4  28908  f1otrge  28927  clwlkclwwlklem2  30058  gsumwun  33139  cyc3genpm  33215  elrgspnlem4  33308  erler  33328  rlocaddval  33331  rlocmulval  33332  rloccring  33333  rhmquskerlem  33487  elrspunidl  33490  rhmimaidl  33494  ssdifidllem  33518  ssdifidlprm  33520  mxidlirredi  33533  mxidlirred  33534  ssmxidllem  33535  qsdrngi  33557  1arithidom  33599  1arithufdlem3  33608  r1plmhm  33672  r1pquslmic  33673  lbsdiflsp0  33764  dimkerim  33765  fedgmul  33769  fldextrspunlsplem  33811  fldext2chn  33866  constrextdg2lem  33886  txomap  33972  matunitlindflem1  37788  heicant  37827  mblfinlem3  37831  primrootscoprmpow  42390  aks6d1c2lem4  42418  aks6d1c5  42430  limclner  45931  hoidmvle  46880  chnerlem1  47162