MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  stoic1aOLD Structured version   Unicode version

Theorem stoic1aOLD 1652
Description: Obsolete proof of stoic1a 1651 as of 20-May-2020. (Contributed by David A. Wheeler, 16-Feb-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
stoic1.1  |-  ( (
ph  /\  ps )  ->  th )
Assertion
Ref Expression
stoic1aOLD  |-  ( (
ph  /\  -.  th )  ->  -.  ps )

Proof of Theorem stoic1aOLD
StepHypRef Expression
1 stoic1.1 . . . . . 6  |-  ( (
ph  /\  ps )  ->  th )
21con3i 140 . . . . 5  |-  ( -. 
th  ->  -.  ( ph  /\ 
ps ) )
3 ianor 490 . . . . 5  |-  ( -.  ( ph  /\  ps ) 
<->  ( -.  ph  \/  -.  ps ) )
42, 3sylib 199 . . . 4  |-  ( -. 
th  ->  ( -.  ph  \/  -.  ps ) )
54anim2i 571 . . 3  |-  ( (
ph  /\  -.  th )  ->  ( ph  /\  ( -.  ph  \/  -.  ps ) ) )
6 orcom 388 . . . 4  |-  ( ( ( ph  /\  -.  ph )  \/  ( ph  /\ 
-.  ps ) )  <->  ( ( ph  /\  -.  ps )  \/  ( ph  /\  -.  ph ) ) )
7 andi 875 . . . 4  |-  ( (
ph  /\  ( -.  ph  \/  -.  ps )
)  <->  ( ( ph  /\ 
-.  ph )  \/  ( ph  /\  -.  ps )
) )
8 pm3.24 890 . . . . 5  |-  -.  ( ph  /\  -.  ph )
98biorfi 408 . . . 4  |-  ( (
ph  /\  -.  ps )  <->  ( ( ph  /\  -.  ps )  \/  ( ph  /\  -.  ph )
) )
106, 7, 93bitr4i 280 . . 3  |-  ( (
ph  /\  ( -.  ph  \/  -.  ps )
)  <->  ( ph  /\  -.  ps ) )
115, 10sylib 199 . 2  |-  ( (
ph  /\  -.  th )  ->  ( ph  /\  -.  ps ) )
1211simprd 464 1  |-  ( (
ph  /\  -.  th )  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369    /\ wa 370
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 188  df-or 371  df-an 372
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator