Theorem ioran 331

Description: Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Assertion

Ref	Expression
ioran	|- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		df-or 241	. . 3 |- ((ph \/ ps) <-> (-. ph -> ps))
2	1	notbii 204	. 2 |- (-. (ph \/ ps) <-> -. (-. ph -> ps))
3		annim 257	. 2 |- ((-. ph /\ -. ps) <-> -. (-. ph -> ps))
4	2, 3	bitr4i 193	1 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240

This theorem is referenced by:  pm4.56 337  oranOLD 339  pm3.2ni 640  andi 665  dfbi3 733  xor2 736  ecase2d 824  ecase3 825  dn1OLD 856  3ori 1157  ecase23d 1198  3ornot23 1281  19.43 1440  equvini 1531  equviniOLD 1532  2ralor 2250  dfun2 2829  sspr 3144  sotrieqOLD 3617  sotrieq2 3618  wereu 3654  ordtri3OLD 3698  ordtri4OLD 3700  ordnbtwn 3761  dfwe2OLD 3862  dflim3 3930  dflim3OLD 3931  dfrdg2 5141  oalimcl 5242  omlimcl 5257  ordtypelem6 5689  1re 6598  ltxrlt 6669  elnnz 7354  elnnz1 7364  om2uzf1oi 7712  sqrlem13 7935  elcncf 8527  extbas1 10291  nonbooli 11231  cvnbtwn4 11861  irredi 11966  atcvat4i 11969  bnj1222 12995  isprm3 13776  3ioran 13808  3orit 13811  poxp 13949  soxp 13950  frxp 13951  axfelem15 14045  dfon3 14072  albineal 14323  ordtypelem6OLD 15380  ufileu 15573  2ralorOLD 15655  3ornot23VD 16671  cvrat4 17076

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain