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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  poxp3  8142  btwnconn1lem7  36585  btwnconn1lem12  36590  linethru  36645  hlrelat3  40206  cvrval3  40207  2atlt  40233  atbtwnex  40242  1cvratlt  40268  2llnmat  40318  lplnexllnN  40358  4atlem11  40403  lnjatN  40574  lncvrat  40576  lncmp  40577  cdlemd9  41000  dihord5b  42053  dihmeetALTN  42121  dih1dimatlem0  42122  mapdrvallem2  42439  grumnudlem  45015  itsclc0yqsol  49564  itschlc0xyqsol  49567