Theorem simp123 1308

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ax5seglem3  28169  axpasch  28179  exatleN  38213  ps-2b  38291  3atlem1  38292  3atlem2  38293  3atlem4  38295  3atlem5  38296  3atlem6  38297  2llnjaN  38375  2llnjN  38376  4atlem12b  38420  2lplnja  38428  2lplnj  38429  dalemrea  38437  dath2  38546  lneq2at  38587  osumcllem7N  38771  cdleme26ee  39169  cdlemg35  39522  cdlemg36  39523  cdlemj1  39630  cdlemk23-3  39711  cdlemk25-3  39713  cdlemk26b-3  39714  cdlemk27-3  39716  cdlemk28-3  39717  cdleml3N  39787  iscnrm3llem2  47485