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  8149  btwnconn1lem7  36676  btwnconn1lem12  36681  linethru  36736  hlrelat3  40288  cvrval3  40289  2atlt  40315  atbtwnex  40324  1cvratlt  40350  2llnmat  40400  lplnexllnN  40440  4atlem11  40485  lnjatN  40656  lncvrat  40658  lncmp  40659  cdlemd9  41082  dihord5b  42135  dihmeetALTN  42203  dih1dimatlem0  42204  mapdrvallem2  42521  grumnudlem  45112  itsclc0yqsol  49697  itschlc0xyqsol  49700