This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem consensus

Description: The consensus theorem. This theorem and its dual (with \/ and /\ interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term ( ps /\ ch ) on the left-hand side is redundant. (Contributed by NM, 16-May-2003) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Wolf Lammen, 20-Jan-2013)

Ref Expression
Assertion consensus 
|- ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2 orc 
 |-  ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
3 2 adantrr 
 |-  ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
4 olc 
 |-  ( ( -. ph /\ ch ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
5 4 adantrl 
 |-  ( ( -. ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
6 3 5 pm2.61ian 
 |-  ( ( ps /\ ch ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
7 1 6 jaoi 
 |-  ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
8 orc 
 |-  ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) )
9 7 8 impbii 
 |-  ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )