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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad7antr  734  ad7antlr  735  simp-6l  783  catass  16790  funcpropd  17003  natpropd  17079  restutop  22533  utopreg  22548  restmetu  22867  lgamucov  25301  istrkgcb  25928  tgifscgr  25980  tgbtwnconn1lem3  26046  legtrd  26061  miriso  26142  footexALT  26190  footex  26193  opphllem3  26221  opphl  26226  trgcopy  26276  cgratr  26295  dfcgra2  26302  inaghl  26318  cgrg3col4  26326  f1otrge  26345  clwlkclwwlklem2  27464  cyc3genpm  30428  lbsdiflsp0  30622  dimkerim  30623  fedgmul  30627  matunitlindflem1  34440  heicant  34479  mblfinlem3  34483  limclner  41495  hoidmvle  42446