Theorem simp122 1304

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

Assertion

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

Proof of Theorem simp122

Step	Hyp	Ref	Expression
1		simp22 1205	. 2 ⊢ ((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) → 𝜓)
2	1	3ad2ant1 1131	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ax5seglem3  27202  axpasch  27212  exatleN  37345  ps-2b  37423  3atlem1  37424  3atlem2  37425  3atlem4  37427  3atlem5  37428  3atlem6  37429  2llnjaN  37507  4atlem12b  37552  2lplnja  37560  dalemqea  37568  dath2  37678  lneq2at  37719  llnexchb2  37810  dalawlem1  37812  lhpexle3lem  37952  cdleme26ee  38301  cdlemg34  38653  cdlemg35  38654  cdlemg36  38655  cdlemj1  38762  cdlemj2  38763  cdlemk23-3  38843  cdlemk25-3  38845  cdlemk26b-3  38846  cdlemk26-3  38847  cdleml3N  38919  iscnrm3llem2  46132