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  8685  lsmcv  19915  archiabl  30829  trisegint  33491  linethru  33616  hlrelat3  36550  cvrval3  36551  cvrval4N  36552  2atlt  36577  atbtwnex  36586  1cvratlt  36612  atcvrlln2  36657  atcvrlln  36658  2llnmat  36662  lplnexllnN  36702  lvolnlelpln  36723  lnjatN  36918  lncvrat  36920  lncmp  36921  cdlemd9  37344  dihord5b  38397  dihmeetALTN  38465  dih1dimatlem0  38466  mapdrvallem2  38783  grumnudlem  40628