Theorem ad6antr 734

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad7antr  736  ad7antlr  737  simp-6l  785  catass  16959  funcpropd  17172  natpropd  17248  restutop  22848  utopreg  22863  restmetu  23182  lgamucov  25617  istrkgcb  26244  tgifscgr  26296  tgbtwnconn1lem3  26362  legtrd  26377  miriso  26458  footexALT  26506  footex  26509  opphllem3  26537  opphl  26542  trgcopy  26592  cgratr  26611  dfcgra2  26618  inaghl  26633  cgrg3col4  26641  f1otrge  26660  clwlkclwwlklem2  27780  cyc3genpm  30796  ssmxidllem  30980  lbsdiflsp0  31024  dimkerim  31025  fedgmul  31029  txomap  31100  matunitlindflem1  34890  heicant  34929  mblfinlem3  34933  limclner  41939  hoidmvle  42889