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  17621  funcpropd  17838  natpropd  17915  ghmqusnsg  19223  ghmquskerlem3  19227  rhmqusnsg  21252  restutop  24193  utopreg  24208  restmetu  24526  lgamucov  27016  istrkgcb  28540  tgifscgr  28592  tgbtwnconn1lem3  28658  legtrd  28673  miriso  28754  footexALT  28802  footex  28805  opphllem3  28833  opphl  28838  trgcopy  28888  cgratr  28907  dfcgra2  28914  inaghl  28929  cgrg3col4  28937  f1otrge  28956  clwlkclwwlklem2  30087  gsumwun  33169  cyc3genpm  33245  elrgspnlem4  33338  erler  33358  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rhmquskerlem  33517  elrspunidl  33520  rhmimaidl  33524  ssdifidllem  33548  ssdifidlprm  33550  mxidlirredi  33563  mxidlirred  33564  ssmxidllem  33565  qsdrngi  33587  1arithidom  33629  1arithufdlem3  33638  r1plmhm  33702  r1pquslmic  33703  lbsdiflsp0  33803  dimkerim  33804  fedgmul  33808  fldextrspunlsplem  33850  fldext2chn  33905  constrextdg2lem  33925  txomap  34011  matunitlindflem1  37864  heicant  37903  mblfinlem3  37907  primrootscoprmpow  42466  aks6d1c2lem4  42494  aks6d1c5  42506  limclner  46006  hoidmvle  46955  chnerlem1  47237