simp112 - Metamath Proof Explorer

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

Theorem simp112 1300

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

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

**Proof of Theorem simp112**
Step	Hyp	Ref	Expression
1		simp12 1201	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)
2	1	3ad2ant1 1130	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1084

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 395 df-3an 1086

This theorem is referenced by: axcontlem4 28798 ps-2b 38987 llncvrlpln2 39062 4atlem11b 39113 4atlem12b 39116 2lnat 39289 cdlemblem 39298 4atexlemex6 39579 cdleme24 39857 cdleme26ee 39865 cdlemg2idN 40101 cdlemg31c 40204 cdlemk26-3 40411 dihglblem2N 40799 0ellimcdiv 45066

	
		OSZAR »