Theorem simp1l3 1266

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  poxp3  8138  btwnconn1lem7  35369  btwnconn1lem12  35374  linethru  35429  hlrelat3  38586  cvrval3  38587  2atlt  38613  atbtwnex  38622  1cvratlt  38648  2llnmat  38698  lplnexllnN  38738  4atlem11  38783  lnjatN  38954  lncvrat  38956  lncmp  38957  cdlemd9  39380  dihord5b  40433  dihmeetALTN  40501  dih1dimatlem0  40502  mapdrvallem2  40819  grumnudlem  43346  itsclc0yqsol  47537  itschlc0xyqsol  47540