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  16957  funcpropd  17170  natpropd  17246  restutop  22846  utopreg  22861  restmetu  23180  lgamucov  25615  istrkgcb  26242  tgifscgr  26294  tgbtwnconn1lem3  26360  legtrd  26375  miriso  26456  footexALT  26504  footex  26507  opphllem3  26535  opphl  26540  trgcopy  26590  cgratr  26609  dfcgra2  26616  inaghl  26631  cgrg3col4  26639  f1otrge  26658  clwlkclwwlklem2  27778  cyc3genpm  30794  ssmxidllem  30978  lbsdiflsp0  31022  dimkerim  31023  fedgmul  31027  txomap  31098  matunitlindflem1  34903  heicant  34942  mblfinlem3  34946  limclner  41952  hoidmvle  42902