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  8160  mapxpen  9155  hash7g  14624  lsmcv  21412  ltslpss  28287  archiabl  33752  trisegint  36773  linethru  36898  hlrelat3  40449  cvrval3  40450  cvrval4N  40451  2atlt  40476  atbtwnex  40485  1cvratlt  40511  atcvrlln2  40556  atcvrlln  40557  2llnmat  40561  lplnexllnN  40601  lvolnlelpln  40622  lnjatN  40817  lncvrat  40819  lncmp  40820  cdlemd9  41243  dihord5b  42296  dihmeetALTN  42364  dih1dimatlem0  42365  mapdrvallem2  42682  grumnudlem  45254