Theorem simp1l3 1270

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

Assertion

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

Proof of Theorem simp1l3

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

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

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 1089

This theorem is referenced by:  poxp3  8094  btwnconn1lem7  36294  btwnconn1lem12  36299  linethru  36354  hlrelat3  39875  cvrval3  39876  2atlt  39902  atbtwnex  39911  1cvratlt  39937  2llnmat  39987  lplnexllnN  40027  4atlem11  40072  lnjatN  40243  lncvrat  40245  lncmp  40246  cdlemd9  40669  dihord5b  41722  dihmeetALTN  41790  dih1dimatlem0  41791  mapdrvallem2  42108  grumnudlem  44733  itsclc0yqsol  49255  itschlc0xyqsol  49258