Theorem simp1l3 1267

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  btwnconn1lem7  34392  btwnconn1lem12  34397  linethru  34452  hlrelat3  37423  cvrval3  37424  2atlt  37450  atbtwnex  37459  1cvratlt  37485  2llnmat  37535  lplnexllnN  37575  4atlem11  37620  lnjatN  37791  lncvrat  37793  lncmp  37794  cdlemd9  38217  dihord5b  39270  dihmeetALTN  39338  dih1dimatlem0  39339  mapdrvallem2  39656  grumnudlem  41873  itsclc0yqsol  46077  itschlc0xyqsol  46080