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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  poxp3  8142  mapxpen  9127  hash7g  14519  lsmcv  21265  ltslpss  28101  archiabl  33518  trisegint  36520  linethru  36645  hlrelat3  40186  cvrval3  40187  cvrval4N  40188  2atlt  40213  atbtwnex  40222  1cvratlt  40248  atcvrlln2  40293  atcvrlln  40294  2llnmat  40298  lplnexllnN  40338  lvolnlelpln  40359  lnjatN  40554  lncvrat  40556  lncmp  40557  cdlemd9  40980  dihord5b  42033  dihmeetALTN  42101  dih1dimatlem0  42102  mapdrvallem2  42419  grumnudlem  44995