Theorem ad6antr 735

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 733	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  737  ad7antlr  738  simp-6l  786  catass  17744  funcpropd  17967  natpropd  18046  ghmqusnsg  19322  ghmquskerlem3  19326  rhmqusnsg  21318  restutop  24267  utopreg  24282  restmetu  24604  lgamucov  27099  istrkgcb  28482  tgifscgr  28534  tgbtwnconn1lem3  28600  legtrd  28615  miriso  28696  footexALT  28744  footex  28747  opphllem3  28775  opphl  28780  trgcopy  28830  cgratr  28849  dfcgra2  28856  inaghl  28871  cgrg3col4  28879  f1otrge  28898  clwlkclwwlklem2  30032  cyc3genpm  33145  erler  33237  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rhmquskerlem  33418  elrspunidl  33421  rhmimaidl  33425  ssdifidllem  33449  ssdifidlprm  33451  mxidlirredi  33464  mxidlirred  33465  ssmxidllem  33466  qsdrngi  33488  1arithidom  33530  1arithufdlem3  33539  r1plmhm  33595  r1pquslmic  33596  lbsdiflsp0  33639  dimkerim  33640  fedgmul  33644  txomap  33780  matunitlindflem1  37576  heicant  37615  mblfinlem3  37619  primrootscoprmpow  42056  aks6d1c2lem4  42084  aks6d1c5  42096  limclner  45572  hoidmvle  46521