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  17654  funcpropd  17871  natpropd  17948  ghmqusnsg  19221  ghmquskerlem3  19225  rhmqusnsg  21202  restutop  24132  utopreg  24147  restmetu  24465  lgamucov  26955  istrkgcb  28390  tgifscgr  28442  tgbtwnconn1lem3  28508  legtrd  28523  miriso  28604  footexALT  28652  footex  28655  opphllem3  28683  opphl  28688  trgcopy  28738  cgratr  28757  dfcgra2  28764  inaghl  28779  cgrg3col4  28787  f1otrge  28806  clwlkclwwlklem2  29936  gsumwun  33012  cyc3genpm  33116  elrgspnlem4  33203  erler  33223  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rhmquskerlem  33403  elrspunidl  33406  rhmimaidl  33410  ssdifidllem  33434  ssdifidlprm  33436  mxidlirredi  33449  mxidlirred  33450  ssmxidllem  33451  qsdrngi  33473  1arithidom  33515  1arithufdlem3  33524  r1plmhm  33582  r1pquslmic  33583  lbsdiflsp0  33629  dimkerim  33630  fedgmul  33634  fldextrspunlsplem  33675  fldext2chn  33725  constrextdg2lem  33745  txomap  33831  matunitlindflem1  37617  heicant  37656  mblfinlem3  37660  primrootscoprmpow  42094  aks6d1c2lem4  42122  aks6d1c5  42134  limclner  45656  hoidmvle  46605