Metamath Proof Explorer

Theorem 3orcomb

Description: Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011) (Proof shortened by Wolf Lammen, 8-Apr-2022)

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

Proof

Step Hyp Ref Expression
1 3orcoma 
 |-  ( ( ph \/ ps \/ ch ) <-> ( ps \/ ph \/ ch ) )
2 3orrot 
 |-  ( ( ps \/ ph \/ ch ) <-> ( ph \/ ch \/ ps ) )
3 1 2 bitri 
 |-  ( ( ph \/ ps \/ ch ) <-> ( ph \/ ch \/ ps ) )