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

Theorem ioran 742
 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 771, anordc 941, or ianordc 885. 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

Proof of Theorem ioran
StepHypRef Expression
1 pm2.45 728 . . 3
2 pm2.46 729 . . 3
31, 2jca 304 . 2
4 simpl 108 . . . . 5
54con2i 617 . . . 4
6 simpr 109 . . . . 5
76con2i 617 . . . 4
85, 7jaoi 706 . . 3
98con2i 617 . 2
103, 9impbii 125 1
 Colors of variables: wff set class Syntax hints:   wn 3   wa 103   wb 104   wo 698 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 This theorem is referenced by:  pm4.56  770  nnexmid  836  dcor  920  3ioran  978  3ori  1279  unssdif  3318  difundi  3335  dcun  3480  sotricim  4256  sotritrieq  4258  en2lp  4480  poxp  6141  nntri2  6402  finexdc  6808  unfidisj  6827  fidcenumlemrks  6858  pw1nel3  7111  sucpw1nel3  7113  onntri45  7120  aptipr  7502  lttri3  7897  letr  7900  apirr  8420  apti  8437  elnnz  9117  xrlttri3  9642  xrletr  9650  exp3val  10355  bcval4  10559  hashunlem  10611  maxleast  11046  xrmaxlesup  11089  lcmval  11816  lcmcllem  11820  lcmgcdlem  11830  isprm3  11871  ivthinc  12865  bj-nnor  13153  pwtrufal  13409  pwle2  13410
 Copyright terms: Public domain W3C validator