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  787  catass  17731  funcpropd  17954  natpropd  18033  ghmqusnsg  19313  ghmquskerlem3  19317  rhmqusnsg  21313  restutop  24262  utopreg  24277  restmetu  24599  lgamucov  27096  istrkgcb  28479  tgifscgr  28531  tgbtwnconn1lem3  28597  legtrd  28612  miriso  28693  footexALT  28741  footex  28744  opphllem3  28772  opphl  28777  trgcopy  28827  cgratr  28846  dfcgra2  28853  inaghl  28868  cgrg3col4  28876  f1otrge  28895  clwlkclwwlklem2  30029  gsumwun  33051  cyc3genpm  33155  elrgspnlem4  33235  erler  33252  rlocaddval  33255  rlocmulval  33256  rloccring  33257  rhmquskerlem  33433  elrspunidl  33436  rhmimaidl  33440  ssdifidllem  33464  ssdifidlprm  33466  mxidlirredi  33479  mxidlirred  33480  ssmxidllem  33481  qsdrngi  33503  1arithidom  33545  1arithufdlem3  33554  r1plmhm  33610  r1pquslmic  33611  lbsdiflsp0  33654  dimkerim  33655  fedgmul  33659  txomap  33795  matunitlindflem1  37603  heicant  37642  mblfinlem3  37646  primrootscoprmpow  42081  aks6d1c2lem4  42109  aks6d1c5  42121  limclner  45607  hoidmvle  46556