Theorem df3an2

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

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

Proof

Step	Hyp	Ref	Expression
1		df-3an	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		df-an	|- ( ( ( ph /\ ps ) /\ ch ) <-> -. ( ( ph /\ ps ) -> -. ch ) )
3		impexp	|- ( ( ( ph /\ ps ) -> -. ch ) <-> ( ph -> ( ps -> -. ch ) ) )
4	2 3	xchbinx	|- ( ( ( ph /\ ps ) /\ ch ) <-> -. ( ph -> ( ps -> -. ch ) ) )
5	1 4	bitri	|- ( ( ph /\ ps /\ ch ) <-> -. ( ph -> ( ps -> -. ch ) ) )