Theorem simp1l3 1283

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  poxp3  8131  btwnconn1lem7  36444  btwnconn1lem12  36449  linethru  36504  hlrelat3  40037  cvrval3  40038  2atlt  40064  atbtwnex  40073  1cvratlt  40099  2llnmat  40149  lplnexllnN  40189  4atlem11  40234  lnjatN  40405  lncvrat  40407  lncmp  40408  cdlemd9  40831  dihord5b  41884  dihmeetALTN  41952  dih1dimatlem0  41953  mapdrvallem2  42270  grumnudlem  44862  itsclc0yqsol  49387  itschlc0xyqsol  49390