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

Theorem ioran 702
Description: Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 841, anordc 898, or ianordc 833. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
ioran  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )

Proof of Theorem ioran
StepHypRef Expression
1 pm2.45 690 . . 3  |-  ( -.  ( ph  \/  ps )  ->  -.  ph )
2 pm2.46 691 . . 3  |-  ( -.  ( ph  \/  ps )  ->  -.  ps )
31, 2jca 300 . 2  |-  ( -.  ( ph  \/  ps )  ->  ( -.  ph  /\ 
-.  ps ) )
4 simpl 107 . . . . 5  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ph )
54con2i 590 . . . 4  |-  ( ph  ->  -.  ( -.  ph  /\ 
-.  ps ) )
6 simpr 108 . . . . 5  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ps )
76con2i 590 . . . 4  |-  ( ps 
->  -.  ( -.  ph  /\ 
-.  ps ) )
85, 7jaoi 669 . . 3  |-  ( (
ph  \/  ps )  ->  -.  ( -.  ph  /\ 
-.  ps ) )
98con2i 590 . 2  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ( ph  \/  ps ) )
103, 9impbii 124 1  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 102    <-> wb 103    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm4.56  840  dcor  877  3ioran  935  3ori  1232  unssdif  3206  difundi  3223  sotricim  4086  sotritrieq  4088  en2lp  4305  poxp  5884  nntri2  6138  unfidisj  6442  aptipr  6893  lttri3  7258  letr  7261  apirr  7772  apti  7789  elnnz  8442  xrlttri3  8948  xrletr  8954  expival  9575  bcval4  9776  sizeunlem  9828  maxleast  10237  lcmval  10589  lcmcllem  10593  lcmgcdlem  10603  isprm3  10644  nnexmid  10721
  Copyright terms: Public domain W3C validator