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  8090  btwnconn1lem7  36236  btwnconn1lem12  36241  linethru  36296  hlrelat3  39611  cvrval3  39612  2atlt  39638  atbtwnex  39647  1cvratlt  39673  2llnmat  39723  lplnexllnN  39763  4atlem11  39808  lnjatN  39979  lncvrat  39981  lncmp  39982  cdlemd9  40405  dihord5b  41458  dihmeetALTN  41526  dih1dimatlem0  41527  mapdrvallem2  41844  grumnudlem  44468  itsclc0yqsol  48952  itschlc0xyqsol  48955