Theorem simp1l3 1360

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  btwnconn1lem7  32519  btwnconn1lem12  32524  linethru  32579  hlrelat3  35190  cvrval3  35191  2atlt  35217  atbtwnex  35226  1cvratlt  35252  2llnmat  35302  lplnexllnN  35342  4atlem11  35387  lnjatN  35558  lncvrat  35560  lncmp  35561  cdlemd9  35985  dihord5b  37038  dihmeetALTN  37106  dih1dimatlem0  37107  mapdrvallem2  37424