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  26719  axpasch  26729  exatleN  36542  ps-2b  36620  3atlem1  36621  3atlem2  36622  3atlem4  36624  3atlem5  36625  3atlem6  36626  2llnjaN  36704  4atlem12b  36749  2lplnja  36757  dalemqea  36765  dath2  36875  lneq2at  36916  llnexchb2  37007  dalawlem1  37009  lhpexle3lem  37149  cdleme26ee  37498  cdlemg34  37850  cdlemg35  37851  cdlemg36  37852  cdlemj1  37959  cdlemj2  37960  cdlemk23-3  38040  cdlemk25-3  38042  cdlemk26b-3  38043  cdlemk26-3  38044  cdleml3N  38116