Theorem simp1l3 1275

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp3  8091  btwnconn1lem7  36330  btwnconn1lem12  36335  linethru  36390  hlrelat3  39913  cvrval3  39914  2atlt  39940  atbtwnex  39949  1cvratlt  39975  2llnmat  40025  lplnexllnN  40065  4atlem11  40110  lnjatN  40281  lncvrat  40283  lncmp  40284  cdlemd9  40707  dihord5b  41760  dihmeetALTN  41828  dih1dimatlem0  41829  mapdrvallem2  42146  grumnudlem  44738  itsclc0yqsol  49263  itschlc0xyqsol  49266