Theorem ad6antr 746

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad7antr  748  ad7antlr  749  simp-6l  796  catass  17708  funcpropd  17925  natpropd  18002  ghmqusnsg  19312  ghmquskerlem3  19316  rhmqusnsg  21342  restutop  24284  utopreg  24299  restmetu  24617  lgamucov  27089  istrkgcb  28612  tgifscgr  28664  tgbtwnconn1lem3  28730  legtrd  28745  miriso  28826  footexALT  28874  footex  28877  opphllem3  28905  opphl  28910  trgcopy  28960  cgratr  28979  dfcgra2  28986  inaghl  29001  cgrg3col4  29009  f1otrge  29028  clwlkclwwlklem2  30158  gsumwun  33216  cyc3genpm  33292  elrgspnlem4  33386  erler  33406  rlocaddval  33410  rlocmulval  33411  rloccring  33412  rhmquskerlem  33571  elrspunidl  33574  rhmimaidl  33578  ssdifidllem  33603  ssdifidlprm  33605  mxidlirredi  33619  mxidlirred  33620  ssmxidllem  33621  qsdrngi  33643  dflringlem2  33651  1arithidom  33693  1arithufdlem3  33702  r1plmhm  33766  r1pquslmic  33767  lbsdiflsp0  33883  dimkerim  33884  fedgmul  33888  fldextrspunlsplem  33930  fldext2chn  33985  constrextdg2lem  34005  txomap  34091  matunitlindflem1  38075  heicant  38114  mblfinlem3  38118  primrootscoprmpow  42676  aks6d1c2lem4  42704  aks6d1c5  42716  limclner  46185  hoidmvle  47134  chnerlem1  47418