Theorem simp1l3 1352

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  btwnconn1lem7  32530  btwnconn1lem12  32535  linethru  32590  hlrelat3  35213  cvrval3  35214  2atlt  35240  atbtwnex  35249  1cvratlt  35275  2llnmat  35325  lplnexllnN  35365  4atlem11  35410  lnjatN  35581  lncvrat  35583  lncmp  35584  cdlemd9  36008  dihord5b  37062  dihmeetALTN  37130  dih1dimatlem0  37131  mapdrvallem2  37448