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  8129  mapxpen  9107  hash7g  14451  lsmcv  21051  sltlpss  27819  archiabl  33152  trisegint  36016  linethru  36141  hlrelat3  39406  cvrval3  39407  cvrval4N  39408  2atlt  39433  atbtwnex  39442  1cvratlt  39468  atcvrlln2  39513  atcvrlln  39514  2llnmat  39518  lplnexllnN  39558  lvolnlelpln  39579  lnjatN  39774  lncvrat  39776  lncmp  39777  cdlemd9  40200  dihord5b  41253  dihmeetALTN  41321  dih1dimatlem0  41322  mapdrvallem2  41639  grumnudlem  44274