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  8131  mapxpen  9112  hash7g  14457  lsmcv  21057  sltlpss  27825  archiabl  33158  trisegint  36011  linethru  36136  hlrelat3  39401  cvrval3  39402  cvrval4N  39403  2atlt  39428  atbtwnex  39437  1cvratlt  39463  atcvrlln2  39508  atcvrlln  39509  2llnmat  39513  lplnexllnN  39553  lvolnlelpln  39574  lnjatN  39769  lncvrat  39771  lncmp  39772  cdlemd9  40195  dihord5b  41248  dihmeetALTN  41316  dih1dimatlem0  41317  mapdrvallem2  41634  grumnudlem  44267