Theorem simp1l3 1264

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  btwnconn1lem7  33549  btwnconn1lem12  33554  linethru  33609  hlrelat3  36542  cvrval3  36543  2atlt  36569  atbtwnex  36578  1cvratlt  36604  2llnmat  36654  lplnexllnN  36694  4atlem11  36739  lnjatN  36910  lncvrat  36912  lncmp  36913  cdlemd9  37336  dihord5b  38389  dihmeetALTN  38457  dih1dimatlem0  38458  mapdrvallem2  38775  grumnudlem  40614  itsclc0yqsol  44745  itschlc0xyqsol  44748