This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem stoic1b

Description: Stoic logic Thema 1 (part b). The other part of thema 1 of Stoic logic; see stoic1a . (Contributed by David A. Wheeler, 16-Feb-2019)

		Ref	Expression
	Hypothesis	stoic1.1	$⊢ (φ \land ψ) \to θ$
	Assertion	stoic1b	$⊢ (ψ \land \neg θ) \to \neg φ$

Step	Hyp	Ref	Expression
1		stoic1.1	$⊢ (φ \land ψ) \to θ$
2	1	ancoms	$⊢ (ψ \land φ) \to θ$
3	2	stoic1a	$⊢ (ψ \land \neg θ) \to \neg φ$