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

Metamath Proof Explorer

Theorem 3ianor

Description: Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Andrew Salmon, 13-May-2011) Shorten with xchnxbir . (Revised by Wolf Lammen, 8-Apr-2022)

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

Proof

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