Theorem simp123 1314

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

Assertion

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

Proof of Theorem simp123

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ax5seglem3  29018  axpasch  29028  exatleN  39896  ps-2b  39974  3atlem1  39975  3atlem2  39976  3atlem4  39978  3atlem5  39979  3atlem6  39980  2llnjaN  40058  2llnjN  40059  4atlem12b  40103  2lplnja  40111  2lplnj  40112  dalemrea  40120  dath2  40229  lneq2at  40270  osumcllem7N  40454  cdleme26ee  40852  cdlemg35  41205  cdlemg36  41206  cdlemj1  41313  cdlemk23-3  41394  cdlemk25-3  41396  cdlemk26b-3  41397  cdlemk27-3  41399  cdlemk28-3  41400  cdleml3N  41470  iscnrm3llem2  49440