Theorem dfandc 869

Description: Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 626. (Contributed by Jim Kingdon, 30-Apr-2018.)

Assertion

Ref	Expression
dfandc	|- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) ) )

Proof of Theorem dfandc

Step	Hyp	Ref	Expression
1		pm3.2im 626	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 123	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3		simplimdc 845	. . . . . . 7 |- (DECID ph -> ( -. ( ph -> -. ps ) -> ph ) )
4	3	adantr 274	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ph ) )
5	4	imp 123	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ph )
6		simprimdc 844	. . . . . . 7 |- (DECID ps -> ( -. ( ph -> -. ps ) -> ps ) )
7	6	adantl 275	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ps ) )
8	7	imp 123	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ps )
9	5, 8	jca 304	. . . 4 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ( ph /\ ps ) )
10	9	ex 114	. . 3 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ( ph /\ ps ) ) )
11	2, 10	impbid2 142	. 2 |- ( (DECID ph /\ DECID ps ) -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) )
12	11	ex 114	1 |- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104  DECID wdc 819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698

This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820

This theorem is referenced by:  pm4.63dc  871  pm4.54dc  887