Theorem simp1l1 1273

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

Assertion

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

Proof of Theorem simp1l1

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

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

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

This theorem is referenced by:  poxp3  8090  mapxpen  9071  hash7g  14439  lsmcv  21134  ltslpss  27918  archiabl  33279  trisegint  36256  linethru  36381  hlrelat3  39904  cvrval3  39905  cvrval4N  39906  2atlt  39931  atbtwnex  39940  1cvratlt  39966  atcvrlln2  40011  atcvrlln  40012  2llnmat  40016  lplnexllnN  40056  lvolnlelpln  40077  lnjatN  40272  lncvrat  40274  lncmp  40275  cdlemd9  40698  dihord5b  41751  dihmeetALTN  41819  dih1dimatlem0  41820  mapdrvallem2  42137  grumnudlem  44729