Theorem dfandc 884

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 637. (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 637	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 124	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3		simplimdc 860	. . . . . . 7 |- (DECID ph -> ( -. ( ph -> -. ps ) -> ph ) )
4	3	adantr 276	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ph ) )
5	4	imp 124	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ph )
6		simprimdc 859	. . . . . . 7 |- (DECID ps -> ( -. ( ph -> -. ps ) -> ps ) )
7	6	adantl 277	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ps ) )
8	7	imp 124	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ps )
9	5, 8	jca 306	. . . 4 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ( ph /\ ps ) )
10	9	ex 115	. . 3 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ( ph /\ ps ) ) )
11	2, 10	impbid2 143	. 2 |- ( (DECID ph /\ DECID ps ) -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) )
12	11	ex 115	1 |- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835

This theorem is referenced by:  pm4.63dc  886  pm4.54dc  902