Theorem ioran 511

Description: Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Assertion

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

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		pm4.65 443	. 2 |- ( -. ( -. ph -> ps ) <-> ( -. ph /\ -. ps ) )
2		pm4.64 387	. 2 |- ( ( -. ph -> ps ) <-> ( ph \/ ps ) )
3	1, 2	xchnxbi 322	1 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386

This theorem is referenced by:  pm4.56  516  xor  935  3ioran  1056  3ori  1388  ecase23d  1436  19.43OLD  1811  2ralor  3109  dfun2  3859  prnebg  4389  sotrieq2  5063  somo  5069  ordnbtwnOLD  5817  dflim3  7047  frxp  7287  poxp  7289  soxp  7290  oalimcl  7640  omlimcl  7658  oeeulem  7681  domunfican  8233  ordtypelem7  8429  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1  8586  cnfcom2lem  8598  ssfin4  9132  fin1a2lem7  9228  fin1a2lem12  9233  fpwwe2lem13  9464  fpwwe2  9465  r1wunlim  9559  1re  10039  recgt0  10867  elnnz  11387  xrltlen  11979  xaddf  12055  xmullem  12094  xmullem2  12095  ssfzoulel  12562  elfznelfzo  12573  elfznelfzob  12574  om2uzf1oi  12752  fsuppmapnn0fiubex  12792  bcval4  13094  sadcaddlem  15179  lcmcllem  15309  lcmgcdlem  15319  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  isprm3  15396  prm23ge5  15520  pcpremul  15548  subgmulg  17608  isnirred  18700  isdomn2  19299  cnfldfunALT  19759  mdetunilem7  20424  mndifsplit  20442  ordtbaslem  20992  iunconn  21231  fbun  21644  fin1aufil  21736  reconnlem2  22630  rrxmvallem  23187  pmltpc  23219  itg2splitlem  23515  mdegmullem  23838  atans2  24658  leibpilem2  24668  leibpi  24669  wilthlem2  24795  lgsdir2  25055  2lgslem3  25129  ragncol  25604  opptgdim2  25637  hlpasch  25648  trgcopy  25696  cgrg3col4  25734  structiedg0val  25911  usgredg2v  26119  nb3grprlem2  26283  vtxd0nedgb  26384  1egrvtxdg0  26407  wwlksnndef  26800  wwlksnfi  26801  clwwlksnndef  26890  nfrgr2v  27136  nonbooli  28510  cvnbtwn4  29148  chirredi  29253  atcvat4i  29256  bnj1304  30890  bnj1417  31109  erdszelem9  31181  3orit  31596  nosepdmlem  31833  sltrec  31924  dfon3  31999  dfrdg4  32058  poimirlem18  33427  poimirlem21  33430  orsild  33889  orsird  33890  notornotel1  33897  cvrat4  34729  hdmaplem4  37063  mapdh9a  37079  fnwe2lem2  37621  ifpnot23  37823  ifpim123g  37845  df3or2  38060  3ornot23VD  39082  ndisj2  39218  xrssre  39564  icccncfext  40100  fourierdlem42  40366  fourierdlem92  40415  salexct2  40557  nnfoctbdjlem  40672  afvfv0bi  41232  ltnltne  41313  lighneallem4  41527  oddprmALTV  41598  mndpsuppss  42152