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 1135	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒)

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

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  btwnconn1lem7  34081  btwnconn1lem12  34086  linethru  34141  hlrelat3  37112  cvrval3  37113  2atlt  37139  atbtwnex  37148  1cvratlt  37174  2llnmat  37224  lplnexllnN  37264  4atlem11  37309  lnjatN  37480  lncvrat  37482  lncmp  37483  cdlemd9  37906  dihord5b  38959  dihmeetALTN  39027  dih1dimatlem0  39028  mapdrvallem2  39345  grumnudlem  41517  itsclc0yqsol  45726  itschlc0xyqsol  45729