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 
|- ( ( ph /\ ps ) -> th )
Assertion stoic1b 
|- ( ( ps /\ -. th ) -> -. ph )

Proof

Step Hyp Ref Expression
1 stoic1.1 
 |-  ( ( ph /\ ps ) -> th )
2 1 ancoms 
 |-  ( ( ps /\ ph ) -> th )
3 2 stoic1a 
 |-  ( ( ps /\ -. th ) -> -. ph )