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  17610  funcpropd  17827  natpropd  17904  ghmqusnsg  19179  ghmquskerlem3  19183  rhmqusnsg  21210  restutop  24141  utopreg  24156  restmetu  24474  lgamucov  26964  istrkgcb  28419  tgifscgr  28471  tgbtwnconn1lem3  28537  legtrd  28552  miriso  28633  footexALT  28681  footex  28684  opphllem3  28712  opphl  28717  trgcopy  28767  cgratr  28786  dfcgra2  28793  inaghl  28808  cgrg3col4  28816  f1otrge  28835  clwlkclwwlklem2  29962  gsumwun  33031  cyc3genpm  33107  elrgspnlem4  33198  erler  33218  rlocaddval  33221  rlocmulval  33222  rloccring  33223  rhmquskerlem  33375  elrspunidl  33378  rhmimaidl  33382  ssdifidllem  33406  ssdifidlprm  33408  mxidlirredi  33421  mxidlirred  33422  ssmxidllem  33423  qsdrngi  33445  1arithidom  33487  1arithufdlem3  33496  r1plmhm  33554  r1pquslmic  33555  lbsdiflsp0  33601  dimkerim  33602  fedgmul  33606  fldextrspunlsplem  33647  fldext2chn  33697  constrextdg2lem  33717  txomap  33803  matunitlindflem1  37598  heicant  37637  mblfinlem3  37641  primrootscoprmpow  42075  aks6d1c2lem4  42103  aks6d1c5  42115  limclner  45636  hoidmvle  46585