Metamath Proof Explorer

Theorem ne3anior

Description: A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013)

Ref Expression
Assertion ne3anior 
|- ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )

Proof

Step Hyp Ref Expression
1 3anor 
 |-  ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( -. A =/= B \/ -. C =/= D \/ -. E =/= F ) )
2 nne 
 |-  ( -. A =/= B <-> A = B )
3 nne 
 |-  ( -. C =/= D <-> C = D )
4 nne 
 |-  ( -. E =/= F <-> E = F )
5 2 3 4 3orbi123i 
 |-  ( ( -. A =/= B \/ -. C =/= D \/ -. E =/= F ) <-> ( A = B \/ C = D \/ E = F ) )
6 1 5 xchbinx 
 |-  ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )