Theorem simp1l1 1285

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

Assertion

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

Proof of Theorem simp1l1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8204  mapxpen  9200  hash7g  14672  lsmcv  21470  ltslpss  28351  archiabl  33858  trisegint  37008  linethru  37133  hlrelat3  40735  cvrval3  40736  cvrval4N  40737  2atlt  40762  atbtwnex  40771  1cvratlt  40797  atcvrlln2  40842  atcvrlln  40843  2llnmat  40847  lplnexllnN  40887  lvolnlelpln  40908  lnjatN  41103  lncvrat  41105  lncmp  41106  cdlemd9  41529  dihord5b  42582  dihmeetALTN  42650  dih1dimatlem0  42651  mapdrvallem2  42968  grumnudlem  45530