Theorem simp1l3 1287

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

Assertion

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

Proof of Theorem simp1l3

Step	Hyp	Ref	Expression
1		simpl3 1212	. 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  8180  btwnconn1lem7  36988  btwnconn1lem12  36993  linethru  37048  hlrelat3  40612  cvrval3  40613  2atlt  40639  atbtwnex  40648  1cvratlt  40674  2llnmat  40724  lplnexllnN  40764  4atlem11  40809  lnjatN  40980  lncvrat  40982  lncmp  40983  cdlemd9  41406  dihord5b  42459  dihmeetALTN  42527  dih1dimatlem0  42528  mapdrvallem2  42845  grumnudlem  45412  itsclc0yqsol  50018  itschlc0xyqsol  50021