Theorem simp1l1 1246

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  mapxpen  8479  lsmcv  19635  archiabl  30499  trisegint  33016  linethru  33141  hlrelat3  35999  cvrval3  36000  cvrval4N  36001  2atlt  36026  atbtwnex  36035  1cvratlt  36061  atcvrlln2  36106  atcvrlln  36107  2llnmat  36111  lplnexllnN  36151  lvolnlelpln  36172  lnjatN  36367  lncvrat  36369  lncmp  36370  cdlemd9  36793  dihord5b  37846  dihmeetALTN  37914  dih1dimatlem0  37915  mapdrvallem2  38232  grumnudlem  40002