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

Theorem ioran 752
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 781, anordc 956, or ianordc 899. 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 738 . . 3  |-  ( -.  ( ph  \/  ps )  ->  -.  ph )
2 pm2.46 739 . . 3  |-  ( -.  ( ph  \/  ps )  ->  -.  ps )
31, 2jca 306 . 2  |-  ( -.  ( ph  \/  ps )  ->  ( -.  ph  /\ 
-.  ps ) )
4 simpl 109 . . . . 5  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ph )
54con2i 627 . . . 4  |-  ( ph  ->  -.  ( -.  ph  /\ 
-.  ps ) )
6 simpr 110 . . . . 5  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ps )
76con2i 627 . . . 4  |-  ( ps 
->  -.  ( -.  ph  /\ 
-.  ps ) )
85, 7jaoi 716 . . 3  |-  ( (
ph  \/  ps )  ->  -.  ( -.  ph  /\ 
-.  ps ) )
98con2i 627 . 2  |-  ( ( -.  ph  /\  -.  ps )  ->  -.  ( ph  \/  ps ) )
103, 9impbii 126 1  |-  ( -.  ( ph  \/  ps ) 
<->  ( -.  ph  /\  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 104    <-> wb 105    \/ wo 708
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
This theorem is referenced by:  pm4.56  780  nnexmid  850  dcor  935  3ioran  993  3ori  1300  unssdif  3370  difundi  3387  dcun  3533  sotricim  4323  sotritrieq  4325  en2lp  4553  poxp  6232  nntri2  6494  finexdc  6901  unfidisj  6920  fidcenumlemrks  6951  pw1nel3  7229  sucpw1nel3  7231  onntri45  7239  aptipr  7639  lttri3  8035  letr  8038  apirr  8560  apti  8577  elnnz  9261  xrlttri3  9795  xrletr  9806  exp3val  10519  bcval4  10727  hashunlem  10779  maxleast  11217  xrmaxlesup  11262  lcmval  12057  lcmcllem  12061  lcmgcdlem  12071  isprm3  12112  pcpremul  12287  ivthinc  14052  lgsdir2  14365  bj-nnor  14406  pwtrufal  14667  pwle2  14668
  Copyright terms: Public domain W3C validator