Theorem ad6antr 768

Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad6antr	⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad5antr 766	. 2 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
3	2	adantr 480	1 ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad7antr  770  catass  16170  funcpropd  16383  natpropd  16459  restutop  21851  utopreg  21866  restmetu  22185  lgamucov  24564  istrkgcb  25155  tgifscgr  25203  tgbtwnconn1lem3  25269  legtrd  25284  miriso  25365  footex  25413  opphllem3  25441  opphl  25446  trgcopy  25496  cgratr  25515  dfcgra2  25521  inaghl  25531  cgrg3col4  25534  f1otrge  25552  cusgrares  26001  clwlkisclwwlklem1  26315  matunitlindflem1  32575  heicant  32614  mblfinlem3  32618  limclner  38718  hoidmvle  39490  clwlkclwwlklem2  41209