Theorem simp1l1 1279

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp3  8124  mapxpen  9109  hash7g  14493  lsmcv  21199  ltslpss  27989  archiabl  33339  trisegint  36339  linethru  36464  hlrelat3  39997  cvrval3  39998  cvrval4N  39999  2atlt  40024  atbtwnex  40033  1cvratlt  40059  atcvrlln2  40104  atcvrlln  40105  2llnmat  40109  lplnexllnN  40149  lvolnlelpln  40170  lnjatN  40365  lncvrat  40367  lncmp  40368  cdlemd9  40791  dihord5b  41844  dihmeetALTN  41912  dih1dimatlem0  41913  mapdrvallem2  42230  grumnudlem  44822