Theorem simp1l1 1285

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

Assertion

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

Proof of Theorem simp1l1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8171  mapxpen  9167  hash7g  14636  lsmcv  21426  ltslpss  28301  archiabl  33807  trisegint  36887  linethru  37012  hlrelat3  40576  cvrval3  40577  cvrval4N  40578  2atlt  40603  atbtwnex  40612  1cvratlt  40638  atcvrlln2  40683  atcvrlln  40684  2llnmat  40688  lplnexllnN  40728  lvolnlelpln  40749  lnjatN  40944  lncvrat  40946  lncmp  40947  cdlemd9  41370  dihord5b  42423  dihmeetALTN  42491  dih1dimatlem0  42492  mapdrvallem2  42809  grumnudlem  45376