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 ⊢ φ ∧ ψ → θ
Assertion stoic1b ⊢ ψ ∧ ¬ θ → ¬ φ

Proof

Step Hyp Ref Expression
1 stoic1.1 ⊢ φ ∧ ψ → θ
2 1 ancoms ⊢ ψ ∧ φ → θ
3 2 stoic1a ⊢ ψ ∧ ¬ θ → ¬ φ