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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad7antr  738  ad7antlr  739  simp-6l  787  catass  17143  funcpropd  17361  natpropd  17439  restutop  23089  utopreg  23104  restmetu  23422  lgamucov  25874  istrkgcb  26501  tgifscgr  26553  tgbtwnconn1lem3  26619  legtrd  26634  miriso  26715  footexALT  26763  footex  26766  opphllem3  26794  opphl  26799  trgcopy  26849  cgratr  26868  dfcgra2  26875  inaghl  26890  cgrg3col4  26898  f1otrge  26917  clwlkclwwlklem2  28037  cyc3genpm  31092  elrspunidl  31274  rhmimaidl  31277  ssmxidllem  31309  lbsdiflsp0  31375  dimkerim  31376  fedgmul  31380  txomap  31452  matunitlindflem1  35459  heicant  35498  mblfinlem3  35502  limclner  42810  hoidmvle  43756