Metamath Proof Explorer


Theorem df3or2

Description: Express triple-or in terms of implication and negation. Statement in Frege1879 p. 11. (Contributed by RP, 25-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 df-3or
 |-  ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2 df-or
 |-  ( ( ( ph \/ ps ) \/ ch ) <-> ( -. ( ph \/ ps ) -> ch ) )
3 ioran
 |-  ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
4 3 imbi1i
 |-  ( ( -. ( ph \/ ps ) -> ch ) <-> ( ( -. ph /\ -. ps ) -> ch ) )
5 impexp
 |-  ( ( ( -. ph /\ -. ps ) -> ch ) <-> ( -. ph -> ( -. ps -> ch ) ) )
6 4 5 bitri
 |-  ( ( -. ( ph \/ ps ) -> ch ) <-> ( -. ph -> ( -. ps -> ch ) ) )
7 2 6 bitri
 |-  ( ( ( ph \/ ps ) \/ ch ) <-> ( -. ph -> ( -. ps -> ch ) ) )
8 1 7 bitri
 |-  ( ( ph \/ ps \/ ch ) <-> ( -. ph -> ( -. ps -> ch ) ) )