Theorem simp123 1188

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ 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:  ax5seglem3  25611  axpasch  25621  exatleN  33708  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem4  33790  3atlem5  33791  3atlem6  33792  2llnjaN  33870  2llnjN  33871  4atlem12b  33915  2lplnja  33923  2lplnj  33924  dalemrea  33932  dath2  34041  lneq2at  34082  osumcllem7N  34266  cdleme26ee  34666  cdlemg35  35019  cdlemg36  35020  cdlemj1  35127  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211  cdlemk27-3  35213  cdlemk28-3  35214  cdleml3N  35284