ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.14 Structured version   GIF version

Theorem pm3.14 657
Description: Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 792. The converse holds for decidable propositions, as seen at pm3.13dc 854. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
pm3.14 ((¬ φ ¬ ψ) → ¬ (φ ψ))

Proof of Theorem pm3.14
StepHypRef Expression
1 simpl 102 . . 3 ((φ ψ) → φ)
21con3i 549 . 2 φ → ¬ (φ ψ))
3 simpr 103 . . 3 ((φ ψ) → ψ)
43con3i 549 . 2 ψ → ¬ (φ ψ))
52, 4jaoi 623 1 ((¬ φ ¬ ψ) → ¬ (φ ψ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97   wo 616
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 532  ax-in2 533  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm3.1  658  xoranor  1253  difindiss  3168
  Copyright terms: Public domain W3C validator