Theorem simp1l1 1265

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  mapxpen  8983  lsmcv  20474  archiabl  31560  sltlpss  34148  trisegint  34391  linethru  34516  hlrelat3  37638  cvrval3  37639  cvrval4N  37640  2atlt  37665  atbtwnex  37674  1cvratlt  37700  atcvrlln2  37745  atcvrlln  37746  2llnmat  37750  lplnexllnN  37790  lvolnlelpln  37811  lnjatN  38006  lncvrat  38008  lncmp  38009  cdlemd9  38432  dihord5b  39485  dihmeetALTN  39553  dih1dimatlem0  39554  mapdrvallem2  39871  grumnudlem  42131