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  8148  mapxpen  9134  hash7g  14537  lsmcv  21295  ltslpss  28132  archiabl  33558  trisegint  36533  linethru  36658  hlrelat3  40219  cvrval3  40220  cvrval4N  40221  2atlt  40246  atbtwnex  40255  1cvratlt  40281  atcvrlln2  40326  atcvrlln  40327  2llnmat  40331  lplnexllnN  40371  lvolnlelpln  40392  lnjatN  40587  lncvrat  40589  lncmp  40590  cdlemd9  41013  dihord5b  42066  dihmeetALTN  42134  dih1dimatlem0  42135  mapdrvallem2  42452  grumnudlem  45028