Theorem simp1l3 1269

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  poxp3  8136  btwnconn1lem7  35065  btwnconn1lem12  35070  linethru  35125  hlrelat3  38283  cvrval3  38284  2atlt  38310  atbtwnex  38319  1cvratlt  38345  2llnmat  38395  lplnexllnN  38435  4atlem11  38480  lnjatN  38651  lncvrat  38653  lncmp  38654  cdlemd9  39077  dihord5b  40130  dihmeetALTN  40198  dih1dimatlem0  40199  mapdrvallem2  40516  grumnudlem  43044  itsclc0yqsol  47450  itschlc0xyqsol  47453