Theorem ad6antr 736

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 734	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  738  ad7antlr  739  simp-6l  786  catass  17596  funcpropd  17813  natpropd  17890  ghmqusnsg  19198  ghmquskerlem3  19202  rhmqusnsg  21226  restutop  24155  utopreg  24170  restmetu  24488  lgamucov  26978  istrkgcb  28437  tgifscgr  28489  tgbtwnconn1lem3  28555  legtrd  28570  miriso  28651  footexALT  28699  footex  28702  opphllem3  28730  opphl  28735  trgcopy  28785  cgratr  28804  dfcgra2  28811  inaghl  28826  cgrg3col4  28834  f1otrge  28853  clwlkclwwlklem2  29984  gsumwun  33054  cyc3genpm  33130  elrgspnlem4  33221  erler  33241  rlocaddval  33244  rlocmulval  33245  rloccring  33246  rhmquskerlem  33399  elrspunidl  33402  rhmimaidl  33406  ssdifidllem  33430  ssdifidlprm  33432  mxidlirredi  33445  mxidlirred  33446  ssmxidllem  33447  qsdrngi  33469  1arithidom  33511  1arithufdlem3  33520  r1plmhm  33579  r1pquslmic  33580  lbsdiflsp0  33662  dimkerim  33663  fedgmul  33667  fldextrspunlsplem  33709  fldext2chn  33764  constrextdg2lem  33784  txomap  33870  matunitlindflem1  37679  heicant  37718  mblfinlem3  37722  primrootscoprmpow  42215  aks6d1c2lem4  42243  aks6d1c5  42255  limclner  45776  hoidmvle  46725  chnerlem1  47007