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  17767  funcpropd  17984  natpropd  18061  ghmqusnsg  19383  ghmquskerlem3  19387  rhmqusnsg  21462  ssdifidllem  21521  ssdifidlprm  21523  restutop  24431  utopreg  24446  restmetu  24764  lgamucov  27239  istrkgcb  28762  tgifscgr  28814  tgbtwnconn1lem3  28880  legtrd  28895  miriso  28984  footexALT  29035  footex  29038  opphllem3  29067  opphl  29072  plng3p  29116  trgcopy  29152  cgratr  29171  dfcgra2  29178  ragcgra  29183  ragsupplcgra  29185  inaghl  29199  cgrg3col4  29207  prlngmolem2  29240  f1otrge  29258  clwlkclwwlklem2  30388  gsumwun  33427  cyc3genpm  33503  elrgspnlem4  33596  erler  33616  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rhmquskerlem  33764  elrspunidl  33767  rhmimaidl  33771  mxidlirredi  33785  mxidlirred  33786  ssmxidllem  33787  qsdrngi  33808  dflringlem2  33816  1arithidom  33858  1arithufdlem3  33867  r1plmhm  33930  r1pquslmic  33931  lbsdiflsp0  34047  dimkerim  34048  fedgmul  34052  fldextrspunlsplem  34094  fldext2chn  34149  constrextdg2lem  34169  txomap  34255  matunitlindflem1  38308  heicant  38347  mblfinlem3  38351  primrootscoprmpow  42907  aks6d1c2lem4  42935  aks6d1c5  42947  limclner  46406  hoidmvle  47355  chnerlem1  47639