ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfandc Unicode version

Theorem dfandc 870
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 627. (Contributed by Jim Kingdon, 30-Apr-2018.)
Assertion
Ref Expression
dfandc  |-  (DECID  ph  ->  (DECID  ps 
->  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) ) ) )

Proof of Theorem dfandc
StepHypRef Expression
1 pm3.2im 627 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 123 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
3 simplimdc 846 . . . . . . 7  |-  (DECID  ph  ->  ( -.  ( ph  ->  -. 
ps )  ->  ph )
)
43adantr 274 . . . . . 6  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ph ) )
54imp 123 . . . . 5  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ph )
6 simprimdc 845 . . . . . . 7  |-  (DECID  ps  ->  ( -.  ( ph  ->  -. 
ps )  ->  ps ) )
76adantl 275 . . . . . 6  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ps ) )
87imp 123 . . . . 5  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ps )
95, 8jca 304 . . . 4  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ( ph  /\ 
ps ) )
109ex 114 . . 3  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ( ph  /\  ps ) ) )
112, 10impbid2 142 . 2  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( ( ph  /\ 
ps )  <->  -.  ( ph  ->  -.  ps )
) )
1211ex 114 1  |-  (DECID  ph  ->  (DECID  ps 
->  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104  DECID wdc 820
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 604  ax-in2 605  ax-io 699
This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821
This theorem is referenced by:  pm4.63dc  872  pm4.54dc  888
  Copyright terms: Public domain W3C validator