Theorem simp1l1 1262

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mapxpen  8686  lsmcv  19916  archiabl  30831  trisegint  33493  linethru  33618  hlrelat3  36552  cvrval3  36553  cvrval4N  36554  2atlt  36579  atbtwnex  36588  1cvratlt  36614  atcvrlln2  36659  atcvrlln  36660  2llnmat  36664  lplnexllnN  36704  lvolnlelpln  36725  lnjatN  36920  lncvrat  36922  lncmp  36923  cdlemd9  37346  dihord5b  38399  dihmeetALTN  38467  dih1dimatlem0  38468  mapdrvallem2  38785  grumnudlem  40627