Theorem simp1l1 1283

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp3  8142  mapxpen  9127  hash7g  14519  lsmcv  21239  ltslpss  28063  archiabl  33455  trisegint  36415  linethru  36540  hlrelat3  40071  cvrval3  40072  cvrval4N  40073  2atlt  40098  atbtwnex  40107  1cvratlt  40133  atcvrlln2  40178  atcvrlln  40179  2llnmat  40183  lplnexllnN  40223  lvolnlelpln  40244  lnjatN  40439  lncvrat  40441  lncmp  40442  cdlemd9  40865  dihord5b  41918  dihmeetALTN  41986  dih1dimatlem0  41987  mapdrvallem2  42304  grumnudlem  44882