Theorem simp122 1313

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1214	. 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  4atlem12b  40103  2lplnja  40111  dalemqea  40119  dath2  40229  lneq2at  40270  llnexchb2  40361  dalawlem1  40363  lhpexle3lem  40503  cdleme26ee  40852  cdlemg34  41204  cdlemg35  41205  cdlemg36  41206  cdlemj1  41313  cdlemj2  41314  cdlemk23-3  41394  cdlemk25-3  41396  cdlemk26b-3  41397  cdlemk26-3  41398  cdleml3N  41470  iscnrm3llem2  49440