Theorem simp1l3 1268

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  poxp3  8087  btwnconn1lem7  34754  btwnconn1lem12  34759  linethru  34814  hlrelat3  37948  cvrval3  37949  2atlt  37975  atbtwnex  37984  1cvratlt  38010  2llnmat  38060  lplnexllnN  38100  4atlem11  38145  lnjatN  38316  lncvrat  38318  lncmp  38319  cdlemd9  38742  dihord5b  39795  dihmeetALTN  39863  dih1dimatlem0  39864  mapdrvallem2  40181  grumnudlem  42687  itsclc0yqsol  46970  itschlc0xyqsol  46973