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  8075  mapxpen  9051  hash7g  14388  lsmcv  21073  sltlpss  27848  archiabl  33159  trisegint  36062  linethru  36187  hlrelat3  39451  cvrval3  39452  cvrval4N  39453  2atlt  39478  atbtwnex  39487  1cvratlt  39513  atcvrlln2  39558  atcvrlln  39559  2llnmat  39563  lplnexllnN  39603  lvolnlelpln  39624  lnjatN  39819  lncvrat  39821  lncmp  39822  cdlemd9  40245  dihord5b  41298  dihmeetALTN  41366  dih1dimatlem0  41367  mapdrvallem2  41684  grumnudlem  44318