Theorem ad6antr 749

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad7antr  751  ad7antlr  752  simp-6l  799  catass  17752  funcpropd  17969  natpropd  18046  ghmqusnsg  19362  ghmquskerlem3  19366  rhmqusnsg  21440  ssdifidllem  21499  ssdifidlprm  21501  restutop  24409  utopreg  24424  restmetu  24742  lgamucov  27217  istrkgcb  28740  tgifscgr  28792  tgbtwnconn1lem3  28858  legtrd  28873  miriso  28962  footexALT  29013  footex  29016  opphllem3  29045  opphl  29050  plng3p  29094  trgcopy  29130  cgratr  29149  dfcgra2  29156  ragcgra  29161  ragsupplcgra  29163  inaghl  29177  cgrg3col4  29185  prlngmolem2  29218  f1otrge  29236  clwlkclwwlklem2  30366  gsumwun  33409  cyc3genpm  33485  elrgspnlem4  33578  erler  33598  rlocaddval  33602  rlocmulval  33603  rloccring  33604  rhmquskerlem  33746  elrspunidl  33749  rhmimaidl  33753  mxidlirredi  33767  mxidlirred  33768  ssmxidllem  33769  qsdrngi  33790  dflringlem2  33798  1arithidom  33840  1arithufdlem3  33849  r1plmhm  33912  r1pquslmic  33913  lbsdiflsp0  34029  dimkerim  34030  fedgmul  34034  fldextrspunlsplem  34076  fldext2chn  34131  constrextdg2lem  34151  txomap  34237  matunitlindflem1  38299  heicant  38338  mblfinlem3  38342  primrootscoprmpow  42898  aks6d1c2lem4  42926  aks6d1c5  42938  limclner  46397  hoidmvle  47346  chnerlem1  47630