Theorem simp123 1309

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  ax5seglem3  26976  axpasch  26986  exatleN  37104  ps-2b  37182  3atlem1  37183  3atlem2  37184  3atlem4  37186  3atlem5  37187  3atlem6  37188  2llnjaN  37266  2llnjN  37267  4atlem12b  37311  2lplnja  37319  2lplnj  37320  dalemrea  37328  dath2  37437  lneq2at  37478  osumcllem7N  37662  cdleme26ee  38060  cdlemg35  38413  cdlemg36  38414  cdlemj1  38521  cdlemk23-3  38602  cdlemk25-3  38604  cdlemk26b-3  38605  cdlemk27-3  38607  cdlemk28-3  38608  cdleml3N  38678  iscnrm3llem2  45860