Theorem ad6antr 748

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 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 746	1 ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad7antr  750  ad7antlr  751  simp-6l  798  catass  17730  funcpropd  17947  natpropd  18024  ghmqusnsg  19340  ghmquskerlem3  19344  rhmqusnsg  21384  ssdifidllem  21441  ssdifidlprm  21443  restutop  24351  utopreg  24366  restmetu  24684  lgamucov  27156  istrkgcb  28679  tgifscgr  28731  tgbtwnconn1lem3  28797  legtrd  28812  miriso  28897  footexALT  28945  footex  28948  opphllem3  28976  opphl  28981  plng3p  29019  trgcopy  29052  cgratr  29071  dfcgra2  29078  inaghl  29093  cgrg3col4  29101  f1otrge  29126  clwlkclwwlklem2  30256  gsumwun  33304  cyc3genpm  33380  elrgspnlem4  33473  erler  33493  rlocaddval  33497  rlocmulval  33498  rloccring  33499  rhmquskerlem  33644  elrspunidl  33647  rhmimaidl  33651  mxidlirredi  33666  mxidlirred  33667  ssmxidllem  33668  qsdrngi  33689  dflringlem2  33697  1arithidom  33739  1arithufdlem3  33748  r1plmhm  33811  r1pquslmic  33812  lbsdiflsp0  33928  dimkerim  33929  fedgmul  33933  fldextrspunlsplem  33975  fldext2chn  34030  constrextdg2lem  34050  txomap  34136  matunitlindflem1  38122  heicant  38161  mblfinlem3  38165  primrootscoprmpow  42723  aks6d1c2lem4  42751  aks6d1c5  42763  limclner  46224  hoidmvle  47173  chnerlem1  47457