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  17592  funcpropd  17809  natpropd  17886  ghmqusnsg  19195  ghmquskerlem3  19199  rhmqusnsg  21223  restutop  24153  utopreg  24168  restmetu  24486  lgamucov  26976  istrkgcb  28435  tgifscgr  28487  tgbtwnconn1lem3  28553  legtrd  28568  miriso  28649  footexALT  28697  footex  28700  opphllem3  28728  opphl  28733  trgcopy  28783  cgratr  28802  dfcgra2  28809  inaghl  28824  cgrg3col4  28832  f1otrge  28851  clwlkclwwlklem2  29978  gsumwun  33043  cyc3genpm  33119  elrgspnlem4  33210  erler  33230  rlocaddval  33233  rlocmulval  33234  rloccring  33235  rhmquskerlem  33388  elrspunidl  33391  rhmimaidl  33395  ssdifidllem  33419  ssdifidlprm  33421  mxidlirredi  33434  mxidlirred  33435  ssmxidllem  33436  qsdrngi  33458  1arithidom  33500  1arithufdlem3  33509  r1plmhm  33568  r1pquslmic  33569  lbsdiflsp0  33637  dimkerim  33638  fedgmul  33642  fldextrspunlsplem  33684  fldext2chn  33739  constrextdg2lem  33759  txomap  33845  matunitlindflem1  37662  heicant  37701  mblfinlem3  37705  primrootscoprmpow  42138  aks6d1c2lem4  42166  aks6d1c5  42178  limclner  45695  hoidmvle  46644