Metamath Proof Explorer

Theorem 3ioran

Description: Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 ioran 
 |-  ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
2 1 anbi1i 
 |-  ( ( -. ( ph \/ ps ) /\ -. ch ) <-> ( ( -. ph /\ -. ps ) /\ -. ch ) )
3 ioran 
 |-  ( -. ( ( ph \/ ps ) \/ ch ) <-> ( -. ( ph \/ ps ) /\ -. ch ) )
4 df-3or 
 |-  ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
5 3 4 xchnxbir 
 |-  ( -. ( ph \/ ps \/ ch ) <-> ( -. ( ph \/ ps ) /\ -. ch ) )
6 df-3an 
 |-  ( ( -. ph /\ -. ps /\ -. ch ) <-> ( ( -. ph /\ -. ps ) /\ -. ch ) )
7 2 5 6 3bitr4i 
 |-  ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) )