Theorem simp1l3 1285

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp3  8146  btwnconn1lem7  36518  btwnconn1lem12  36523  linethru  36578  hlrelat3  40110  cvrval3  40111  2atlt  40137  atbtwnex  40146  1cvratlt  40172  2llnmat  40222  lplnexllnN  40262  4atlem11  40307  lnjatN  40478  lncvrat  40480  lncmp  40481  cdlemd9  40904  dihord5b  41957  dihmeetALTN  42025  dih1dimatlem0  42026  mapdrvallem2  42343  grumnudlem  44921  itsclc0yqsol  49463  itschlc0xyqsol  49466