Theorem ad6antr 742

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad7antr  744  ad7antlr  745  simp-6l  792  catass  17650  funcpropd  17867  natpropd  17944  ghmqusnsg  19255  ghmquskerlem3  19259  rhmqusnsg  21285  restutop  24227  utopreg  24242  restmetu  24560  lgamucov  27026  istrkgcb  28549  tgifscgr  28601  tgbtwnconn1lem3  28667  legtrd  28682  miriso  28763  footexALT  28811  footex  28814  opphllem3  28842  opphl  28847  trgcopy  28897  cgratr  28916  dfcgra2  28923  inaghl  28938  cgrg3col4  28946  f1otrge  28965  clwlkclwwlklem2  30095  gsumwun  33164  cyc3genpm  33240  elrgspnlem4  33333  erler  33353  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rhmquskerlem  33515  elrspunidl  33518  rhmimaidl  33522  ssdifidllem  33546  ssdifidlprm  33548  mxidlirredi  33561  mxidlirred  33562  ssmxidllem  33563  qsdrngi  33585  1arithidom  33627  1arithufdlem3  33636  r1plmhm  33700  r1pquslmic  33701  lbsdiflsp0  33817  dimkerim  33818  fedgmul  33822  fldextrspunlsplem  33864  fldext2chn  33919  constrextdg2lem  33939  txomap  34025  matunitlindflem1  37990  heicant  38029  mblfinlem3  38033  primrootscoprmpow  42591  aks6d1c2lem4  42619  aks6d1c5  42631  limclner  46101  hoidmvle  47050  chnerlem1  47334