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  8152  btwnconn1lem7  36624  btwnconn1lem12  36629  linethru  36684  hlrelat3  40246  cvrval3  40247  2atlt  40273  atbtwnex  40282  1cvratlt  40308  2llnmat  40358  lplnexllnN  40398  4atlem11  40443  lnjatN  40614  lncvrat  40616  lncmp  40617  cdlemd9  41040  dihord5b  42093  dihmeetALTN  42161  dih1dimatlem0  42162  mapdrvallem2  42479  grumnudlem  45055  itsclc0yqsol  49603  itschlc0xyqsol  49606