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  8106  btwnconn1lem7  36054  btwnconn1lem12  36059  linethru  36114  hlrelat3  39379  cvrval3  39380  2atlt  39406  atbtwnex  39415  1cvratlt  39441  2llnmat  39491  lplnexllnN  39531  4atlem11  39576  lnjatN  39747  lncvrat  39749  lncmp  39750  cdlemd9  40173  dihord5b  41226  dihmeetALTN  41294  dih1dimatlem0  41295  mapdrvallem2  41612  grumnudlem  44247  itsclc0yqsol  48726  itschlc0xyqsol  48729