Theorem dfandc 811

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 598. (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 598	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 122	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3		simplimdc 790	. . . . . . 7 |- (DECID ph -> ( -. ( ph -> -. ps ) -> ph ) )
4	3	adantr 270	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ph ) )
5	4	imp 122	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ph )
6		simprimdc 789	. . . . . . 7 |- (DECID ps -> ( -. ( ph -> -. ps ) -> ps ) )
7	6	adantl 271	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ps ) )
8	7	imp 122	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ps )
9	5, 8	jca 300	. . . 4 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ( ph /\ ps ) )
10	9	ex 113	. . 3 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ( ph /\ ps ) ) )
11	2, 10	impbid2 141	. 2 |- ( (DECID ph /\ DECID ps ) -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) )
12	11	ex 113	1 |- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115  df-dc 776

This theorem is referenced by:  pm4.63dc  813  pm4.54dc  838