Theorem simp1l1 1264

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1l1	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1189	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  mapxpen  8879  lsmcv  20318  archiabl  31354  sltlpss  34014  trisegint  34257  linethru  34382  hlrelat3  37353  cvrval3  37354  cvrval4N  37355  2atlt  37380  atbtwnex  37389  1cvratlt  37415  atcvrlln2  37460  atcvrlln  37461  2llnmat  37465  lplnexllnN  37505  lvolnlelpln  37526  lnjatN  37721  lncvrat  37723  lncmp  37724  cdlemd9  38147  dihord5b  39200  dihmeetALTN  39268  dih1dimatlem0  39269  mapdrvallem2  39586  grumnudlem  41792