Theorem simp132 1305

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

Assertion

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

Proof of Theorem simp132

Step	Hyp	Ref	Expression
1		simp32 1206	. 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  3atlem1  36621  3atlem2  36622  3atlem5  36625  2llnjaN  36704  4atlem11b  36746  4atlem12b  36749  lplncvrlvol2  36753  dalemtea  36768  dath2  36875  cdlemblem  36931  dalawlem1  37009  lhpexle3lem  37149  4atexlemex6  37212  cdleme22f2  37485  cdleme22g  37486  cdlemg7aN  37763  cdlemg34  37850  cdlemj1  37959  cdlemk23-3  38040  cdlemk25-3  38042  cdlemk26b-3  38043