Theorem simp1l1 1265

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

Assertion

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

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1190	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1132	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8141  mapxpen  9149  lsmcv  20988  sltlpss  27748  archiabl  32782  trisegint  35472  linethru  35597  hlrelat3  38750  cvrval3  38751  cvrval4N  38752  2atlt  38777  atbtwnex  38786  1cvratlt  38812  atcvrlln2  38857  atcvrlln  38858  2llnmat  38862  lplnexllnN  38902  lvolnlelpln  38923  lnjatN  39118  lncvrat  39120  lncmp  39121  cdlemd9  39544  dihord5b  40597  dihmeetALTN  40665  dih1dimatlem0  40666  mapdrvallem2  40983  grumnudlem  43510