Theorem simp1l3 1156

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

Assertion

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

Proof of Theorem simp1l3

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

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

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 386  df-3an 1039

This theorem is referenced by:  btwnconn1lem7  32200  btwnconn1lem12  32205  linethru  32260  hlrelat3  34698  cvrval3  34699  2atlt  34725  atbtwnex  34734  1cvratlt  34760  2llnmat  34810  lplnexllnN  34850  4atlem11  34895  lnjatN  35066  lncvrat  35068  lncmp  35069  cdlemd9  35493  dihord5b  36548  dihmeetALTN  36616  dih1dimatlem0  36617  mapdrvallem2  36934