Theorem simp1l3 1275

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp3  8090  btwnconn1lem7  36321  btwnconn1lem12  36326  linethru  36381  hlrelat3  39904  cvrval3  39905  2atlt  39931  atbtwnex  39940  1cvratlt  39966  2llnmat  40016  lplnexllnN  40056  4atlem11  40101  lnjatN  40272  lncvrat  40274  lncmp  40275  cdlemd9  40698  dihord5b  41751  dihmeetALTN  41819  dih1dimatlem0  41820  mapdrvallem2  42137  grumnudlem  44729  itsclc0yqsol  49255  itschlc0xyqsol  49258