Theorem simp1l3 1149

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

Assertion

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

Proof of Theorem simp1l3

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  btwnconn1lem7  31370  btwnconn1lem12  31375  linethru  31430  hlrelat3  33716  cvrval3  33717  2atlt  33743  atbtwnex  33752  1cvratlt  33778  2llnmat  33828  lplnexllnN  33868  4atlem11  33913  lnjatN  34084  lncvrat  34086  lncmp  34087  cdlemd9  34511  dihord5b  35566  dihmeetALTN  35634  dih1dimatlem0  35635  mapdrvallem2  35952