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  17730  funcpropd  17948  natpropd  18025  ghmqusnsg  19301  ghmquskerlem3  19305  rhmqusnsg  21296  restutop  24247  utopreg  24262  restmetu  24584  lgamucov  27082  istrkgcb  28465  tgifscgr  28517  tgbtwnconn1lem3  28583  legtrd  28598  miriso  28679  footexALT  28727  footex  28730  opphllem3  28758  opphl  28763  trgcopy  28813  cgratr  28832  dfcgra2  28839  inaghl  28854  cgrg3col4  28862  f1otrge  28881  clwlkclwwlklem2  30020  gsumwun  33069  cyc3genpm  33173  elrgspnlem4  33250  erler  33270  rlocaddval  33273  rlocmulval  33274  rloccring  33275  rhmquskerlem  33454  elrspunidl  33457  rhmimaidl  33461  ssdifidllem  33485  ssdifidlprm  33487  mxidlirredi  33500  mxidlirred  33501  ssmxidllem  33502  qsdrngi  33524  1arithidom  33566  1arithufdlem3  33575  r1plmhm  33631  r1pquslmic  33632  lbsdiflsp0  33678  dimkerim  33679  fedgmul  33683  fldextrspunlsplem  33724  fldext2chn  33770  constrextdg2lem  33790  txomap  33834  matunitlindflem1  37624  heicant  37663  mblfinlem3  37667  primrootscoprmpow  42101  aks6d1c2lem4  42129  aks6d1c5  42141  limclner  45671  hoidmvle  46620