Theorem simp1l3 1287

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

Assertion

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

Proof of Theorem simp1l3

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8167  btwnconn1lem7  36858  btwnconn1lem12  36863  linethru  36918  hlrelat3  40469  cvrval3  40470  2atlt  40496  atbtwnex  40505  1cvratlt  40531  2llnmat  40581  lplnexllnN  40621  4atlem11  40666  lnjatN  40837  lncvrat  40839  lncmp  40840  cdlemd9  41263  dihord5b  42316  dihmeetALTN  42384  dih1dimatlem0  42385  mapdrvallem2  42702  grumnudlem  45268  itsclc0yqsol  49875  itschlc0xyqsol  49878