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  8129  btwnconn1lem7  36081  btwnconn1lem12  36086  linethru  36141  hlrelat3  39406  cvrval3  39407  2atlt  39433  atbtwnex  39442  1cvratlt  39468  2llnmat  39518  lplnexllnN  39558  4atlem11  39603  lnjatN  39774  lncvrat  39776  lncmp  39777  cdlemd9  40200  dihord5b  41253  dihmeetALTN  41321  dih1dimatlem0  41322  mapdrvallem2  41639  grumnudlem  44274  itsclc0yqsol  48753  itschlc0xyqsol  48756