Theorem simp1l3 1266

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

Assertion

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

Proof of Theorem simp1l3

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  btwnconn1lem7  34322  btwnconn1lem12  34327  linethru  34382  hlrelat3  37353  cvrval3  37354  2atlt  37380  atbtwnex  37389  1cvratlt  37415  2llnmat  37465  lplnexllnN  37505  4atlem11  37550  lnjatN  37721  lncvrat  37723  lncmp  37724  cdlemd9  38147  dihord5b  39200  dihmeetALTN  39268  dih1dimatlem0  39269  mapdrvallem2  39586  grumnudlem  41792  itsclc0yqsol  45998  itschlc0xyqsol  46001