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 ( ( 𝜓 ∧ ¬ 𝜃 ) → ¬ 𝜑 )