Theorem simp1l1 1152

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

Assertion

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

Proof of Theorem simp1l1

Step	Hyp	Ref	Expression
1		simpl1 1062	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1080	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  mapxpen  8070  lsmcv  19060  archiabl  29534  trisegint  31774  linethru  31899  hlrelat3  34175  cvrval3  34176  cvrval4N  34177  2atlt  34202  atbtwnex  34211  1cvratlt  34237  atcvrlln2  34282  atcvrlln  34283  2llnmat  34287  lplnexllnN  34327  lvolnlelpln  34348  lnjatN  34543  lncvrat  34545  lncmp  34546  cdlemd9  34970  dihord5b  36025  dihmeetALTN  36093  dih1dimatlem0  36094  mapdrvallem2  36411