Theorem simp1l3 1269

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

Assertion

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

Proof of Theorem simp1l3

Step	Hyp	Ref	Expression
1		simpl3 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)
2	1	3ad2ant1 1133	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8106  btwnconn1lem7  36074  btwnconn1lem12  36079  linethru  36134  hlrelat3  39399  cvrval3  39400  2atlt  39426  atbtwnex  39435  1cvratlt  39461  2llnmat  39511  lplnexllnN  39551  4atlem11  39596  lnjatN  39767  lncvrat  39769  lncmp  39770  cdlemd9  40193  dihord5b  41246  dihmeetALTN  41314  dih1dimatlem0  41315  mapdrvallem2  41632  grumnudlem  44267  itsclc0yqsol  48746  itschlc0xyqsol  48749