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

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
StepHypRef Expression
1 pm3.2im 637 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 124 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
3 simplimdc 860 . . . . . . 7  |-  (DECID  ph  ->  ( -.  ( ph  ->  -. 
ps )  ->  ph )
)
43adantr 276 . . . . . 6  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ph ) )
54imp 124 . . . . 5  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ph )
6 simprimdc 859 . . . . . . 7  |-  (DECID  ps  ->  ( -.  ( ph  ->  -. 
ps )  ->  ps ) )
76adantl 277 . . . . . 6  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ps ) )
87imp 124 . . . . 5  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ps )
95, 8jca 306 . . . 4  |-  ( ( (DECID 
ph  /\ DECID  ps )  /\  -.  ( ph  ->  -.  ps )
)  ->  ( ph  /\ 
ps ) )
109ex 115 . . 3  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( -.  ( ph  ->  -.  ps )  ->  ( ph  /\  ps ) ) )
112, 10impbid2 143 . 2  |-  ( (DECID  ph  /\ DECID  ps )  ->  ( ( ph  /\ 
ps )  <->  -.  ( ph  ->  -.  ps )
) )
1211ex 115 1  |-  (DECID  ph  ->  (DECID  ps 
->  ( ( ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) ) ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator