Theorem simp1l3 1269

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

Assertion

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

Proof of Theorem simp1l3

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8080  btwnconn1lem7  36137  btwnconn1lem12  36142  linethru  36197  hlrelat3  39521  cvrval3  39522  2atlt  39548  atbtwnex  39557  1cvratlt  39583  2llnmat  39633  lplnexllnN  39673  4atlem11  39718  lnjatN  39889  lncvrat  39891  lncmp  39892  cdlemd9  40315  dihord5b  41368  dihmeetALTN  41436  dih1dimatlem0  41437  mapdrvallem2  41754  grumnudlem  44388  itsclc0yqsol  48875  itschlc0xyqsol  48878