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  8106  mapxpen  9084  hash7g  14427  lsmcv  21027  sltlpss  27795  archiabl  33125  trisegint  35989  linethru  36114  hlrelat3  39379  cvrval3  39380  cvrval4N  39381  2atlt  39406  atbtwnex  39415  1cvratlt  39441  atcvrlln2  39486  atcvrlln  39487  2llnmat  39491  lplnexllnN  39531  lvolnlelpln  39552  lnjatN  39747  lncvrat  39749  lncmp  39750  cdlemd9  40173  dihord5b  41226  dihmeetALTN  41294  dih1dimatlem0  41295  mapdrvallem2  41612  grumnudlem  44247