simp131 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > simp131		Structured version Visualization version GIF version

Theorem simp131 1306

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

**Assertion**
Ref	Expression
simp131	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)

**Proof of Theorem simp131**
Step	Hyp	Ref	Expression
1		simp31 1207	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)

Colors of variables: wff setvar class

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 28741 exatleN 38877 3atlem1 38956 3atlem2 38957 3atlem5 38960 2llnjaN 39039 4atlem11b 39081 4atlem12b 39084 lplncvrlvol2 39088 dalemsea 39102 dath2 39210 cdlemblem 39266 dalawlem1 39344 lhpexle3lem 39484 4atexlemex6 39547 cdleme22f2 39820 cdleme22g 39821 cdlemg7aN 40098 cdlemg34 40185 cdlemj1 40294 cdlemk23-3 40375 cdlemk25-3 40377 cdlemk26b-3 40378 cdleml3N 40451

	
		OSZAR »