Theorem simp1l3 1248

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  btwnconn1lem7  33072  btwnconn1lem12  33077  linethru  33132  hlrelat3  35990  cvrval3  35991  2atlt  36017  atbtwnex  36026  1cvratlt  36052  2llnmat  36102  lplnexllnN  36142  4atlem11  36187  lnjatN  36358  lncvrat  36360  lncmp  36361  cdlemd9  36784  dihord5b  37837  dihmeetALTN  37905  dih1dimatlem0  37906  mapdrvallem2  38223  grumnudlem  39993  itsclc0yqsol  44117  itschlc0xyqsol  44120