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

Theorem condc 843
Description: Contraposition of a decidable proposition.

This theorem swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This theorem (without the decidability condition, of course) is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103) and is Axiom A3 of [Margaris] p. 49. We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning.

(Contributed by Jim Kingdon, 13-Mar-2018.) (Proof shortened by BJ, 18-Nov-2023.)

Assertion
Ref Expression
condc  |-  (DECID  ph  ->  ( ( -.  ph  ->  -. 
ps )  ->  ( ps  ->  ph ) ) )

Proof of Theorem condc
StepHypRef Expression
1 dcstab 834 . 2  |-  (DECID  ph  -> STAB  ph )
2 const 842 . 2  |-  (STAB  ph  ->  ( ( -.  ph  ->  -. 
ps )  ->  ( ps  ->  ph ) ) )
31, 2syl 14 1  |-  (DECID  ph  ->  ( ( -.  ph  ->  -. 
ps )  ->  ( ps  ->  ph ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4  STAB wstab 820  DECID wdc 824
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 821  df-dc 825
This theorem is referenced by:  pm2.18dc  845  con1dc  846  con4biddc  847  pm2.521gdc  858  pm2.521dcALT  860  con34bdc  861  necon4aidc  2402  necon4addc  2404  necon4bddc  2405  necon4ddc  2406  nn0n0n1ge2b  9262  gcdeq0  11899  lcmeq0  11992  pcdvdsb  12240  pc2dvds  12250  pcfac  12269  infpnlem1  12278
  Copyright terms: Public domain W3C validator