Theorem ad6antr 732

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 730	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 206  df-an 396

This theorem is referenced by:  ad7antr  734  ad7antlr  735  simp-6l  783  catass  17312  funcpropd  17532  natpropd  17610  restutop  23297  utopreg  23312  restmetu  23632  lgamucov  26092  istrkgcb  26721  tgifscgr  26773  tgbtwnconn1lem3  26839  legtrd  26854  miriso  26935  footexALT  26983  footex  26986  opphllem3  27014  opphl  27019  trgcopy  27069  cgratr  27088  dfcgra2  27095  inaghl  27110  cgrg3col4  27118  f1otrge  27137  clwlkclwwlklem2  28265  cyc3genpm  31321  elrspunidl  31508  rhmimaidl  31511  ssmxidllem  31543  lbsdiflsp0  31609  dimkerim  31610  fedgmul  31614  txomap  31686  matunitlindflem1  35700  heicant  35739  mblfinlem3  35743  limclner  43082  hoidmvle  44028