Theorem simp1l1 1267

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8090  mapxpen  9067  hash7g  14412  lsmcv  21067  sltlpss  27841  archiabl  33159  trisegint  36021  linethru  36146  hlrelat3  39411  cvrval3  39412  cvrval4N  39413  2atlt  39438  atbtwnex  39447  1cvratlt  39473  atcvrlln2  39518  atcvrlln  39519  2llnmat  39523  lplnexllnN  39563  lvolnlelpln  39584  lnjatN  39779  lncvrat  39781  lncmp  39782  cdlemd9  40205  dihord5b  41258  dihmeetALTN  41326  dih1dimatlem0  41327  mapdrvallem2  41644  grumnudlem  44278