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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad7antr  737  ad7antlr  738  simp-6l  786  catass  17630  funcpropd  17851  natpropd  17929  restutop  23742  utopreg  23757  restmetu  24079  lgamucov  26542  istrkgcb  27707  tgifscgr  27759  tgbtwnconn1lem3  27825  legtrd  27840  miriso  27921  footexALT  27969  footex  27972  opphllem3  28000  opphl  28005  trgcopy  28055  cgratr  28074  dfcgra2  28081  inaghl  28096  cgrg3col4  28104  f1otrge  28123  clwlkclwwlklem2  29253  cyc3genpm  32311  ghmquskerlem3  32531  rhmquskerlem  32543  elrspunidl  32546  rhmimaidl  32550  mxidlirredi  32587  mxidlirred  32588  ssmxidllem  32589  qsdrngi  32609  lbsdiflsp0  32711  dimkerim  32712  fedgmul  32716  txomap  32814  matunitlindflem1  36484  heicant  36523  mblfinlem3  36527  limclner  44367  hoidmvle  45316