Theorem simp1l1 1263

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

Assertion

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

Proof of Theorem simp1l1

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  mapxpen  8667  lsmcv  19906  archiabl  30877  trisegint  33602  linethru  33727  hlrelat3  36708  cvrval3  36709  cvrval4N  36710  2atlt  36735  atbtwnex  36744  1cvratlt  36770  atcvrlln2  36815  atcvrlln  36816  2llnmat  36820  lplnexllnN  36860  lvolnlelpln  36881  lnjatN  37076  lncvrat  37078  lncmp  37079  cdlemd9  37502  dihord5b  38555  dihmeetALTN  38623  dih1dimatlem0  38624  mapdrvallem2  38941  grumnudlem  40993