Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-orel12 Structured version   Visualization version   Unicode version

Theorem wl-orel12 31893
Description: In a conjunctive normal form a pair of nodes like  ( ph  \/  ps )  /\  ( -.  ph  \/  ch ) eliminates the need of a node  ( ps  \/  ch ). This theorem allows simplifications in that respect. (Contributed by Wolf Lammen, 20-Jun-2020.)
Assertion
Ref Expression
wl-orel12  |-  ( ( ( ph  \/  ps )  /\  ( -.  ph  \/  ch ) )  -> 
( ps  \/  ch ) )

Proof of Theorem wl-orel12
StepHypRef Expression
1 pm2.1 423 . 2  |-  ( -. 
ph  \/  ph )
2 orel1 388 . . . 4  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
3 orc 391 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
42, 3syl6com 36 . . 3  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ( ps  \/  ch )
) )
5 notnot1 127 . . . . 5  |-  ( ph  ->  -.  -.  ph )
6 orel1 388 . . . . 5  |-  ( -. 
-.  ph  ->  ( ( -.  ph  \/  ch )  ->  ch ) )
75, 6syl 17 . . . 4  |-  ( ph  ->  ( ( -.  ph  \/  ch )  ->  ch ) )
8 olc 390 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
97, 8syl6com 36 . . 3  |-  ( ( -.  ph  \/  ch )  ->  ( ph  ->  ( ps  \/  ch )
) )
104, 9jaao 516 . 2  |-  ( ( ( ph  \/  ps )  /\  ( -.  ph  \/  ch ) )  -> 
( ( -.  ph  \/  ph )  ->  ( ps  \/  ch ) ) )
111, 10mpi 20 1  |-  ( ( ( ph  \/  ps )  /\  ( -.  ph  \/  ch ) )  -> 
( ps  \/  ch ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 374    /\ wa 375
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 190  df-or 376  df-an 377
This theorem is referenced by:  wl-cases2-dnf  31894
  Copyright terms: Public domain W3C validator