Theorem dfandc 778

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 566. (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 566	. . . 4 |- ( ph -> ( ps -> -. ( ph -> -. ps ) ) )
2	1	imp 115	. . 3 |- ( ( ph /\ ps ) -> -. ( ph -> -. ps ) )
3		simplimdc 757	. . . . . . 7 |- (DECID ph -> ( -. ( ph -> -. ps ) -> ph ) )
4	3	adantr 261	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ph ) )
5	4	imp 115	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ph )
6		simprimdc 756	. . . . . . 7 |- (DECID ps -> ( -. ( ph -> -. ps ) -> ps ) )
7	6	adantl 262	. . . . . 6 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ps ) )
8	7	imp 115	. . . . 5 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ps )
9	5, 8	jca 290	. . . 4 |- ( ( (DECID ph /\ DECID ps ) /\ -. ( ph -> -. ps ) ) -> ( ph /\ ps ) )
10	9	ex 108	. . 3 |- ( (DECID ph /\ DECID ps ) -> ( -. ( ph -> -. ps ) -> ( ph /\ ps ) ) )
11	2, 10	impbid2 131	. 2 |- ( (DECID ph /\ DECID ps ) -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) )
12	11	ex 108	1 |- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 97   <-> wb 98  DECID wdc 742

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630

This theorem depends on definitions:  df-bi 110  df-dc 743

This theorem is referenced by:  pm4.63dc  780  pm4.54dc  805