Theorem simp122 1302

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

Assertion

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

Proof of Theorem simp122

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ax5seglem3  26720  axpasch  26730  exatleN  36544  ps-2b  36622  3atlem1  36623  3atlem2  36624  3atlem4  36626  3atlem5  36627  3atlem6  36628  2llnjaN  36706  4atlem12b  36751  2lplnja  36759  dalemqea  36767  dath2  36877  lneq2at  36918  llnexchb2  37009  dalawlem1  37011  lhpexle3lem  37151  cdleme26ee  37500  cdlemg34  37852  cdlemg35  37853  cdlemg36  37854  cdlemj1  37961  cdlemj2  37962  cdlemk23-3  38042  cdlemk25-3  38044  cdlemk26b-3  38045  cdlemk26-3  38046  cdleml3N  38118