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  9141  hash7g  14551  lsmcv  21328  ltslpss  28173  archiabl  33638  trisegint  36608  linethru  36733  hlrelat3  40285  cvrval3  40286  cvrval4N  40287  2atlt  40312  atbtwnex  40321  1cvratlt  40347  atcvrlln2  40392  atcvrlln  40393  2llnmat  40397  lplnexllnN  40437  lvolnlelpln  40458  lnjatN  40653  lncvrat  40655  lncmp  40656  cdlemd9  41079  dihord5b  42132  dihmeetALTN  42200  dih1dimatlem0  42201  mapdrvallem2  42518  grumnudlem  45109