Theorem ad6antr 748

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 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 746	1 ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad7antr  750  ad7antlr  751  simp-6l  798  catass  17743  funcpropd  17960  natpropd  18037  ghmqusnsg  19353  ghmquskerlem3  19357  rhmqusnsg  21406  ssdifidllem  21465  ssdifidlprm  21467  restutop  24375  utopreg  24390  restmetu  24708  lgamucov  27183  istrkgcb  28706  tgifscgr  28758  tgbtwnconn1lem3  28824  legtrd  28839  miriso  28928  footexALT  28979  footex  28982  opphllem3  29011  opphl  29016  plng3p  29060  trgcopy  29096  cgratr  29115  dfcgra2  29122  ragcgra  29127  ragsupplcgra  29129  inaghl  29143  cgrg3col4  29151  prlngmolem2  29184  f1otrge  29202  clwlkclwwlklem2  30332  gsumwun  33377  cyc3genpm  33453  elrgspnlem4  33546  erler  33566  rlocaddval  33570  rlocmulval  33571  rloccring  33572  rhmquskerlem  33714  elrspunidl  33717  rhmimaidl  33721  mxidlirredi  33735  mxidlirred  33736  ssmxidllem  33737  qsdrngi  33758  dflringlem2  33766  1arithidom  33808  1arithufdlem3  33817  r1plmhm  33880  r1pquslmic  33881  lbsdiflsp0  33997  dimkerim  33998  fedgmul  34002  fldextrspunlsplem  34044  fldext2chn  34099  constrextdg2lem  34119  txomap  34205  matunitlindflem1  38248  heicant  38287  mblfinlem3  38291  primrootscoprmpow  42847  aks6d1c2lem4  42875  aks6d1c5  42887  limclner  46348  hoidmvle  47297  chnerlem1  47581