Theorem ioran 754

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 783, anordc 959, or ianordc 901. 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

Step	Hyp	Ref	Expression
1		pm2.45 740	. . 3 |- ( -. ( ph \/ ps ) -> -. ph )
2		pm2.46 741	. . 3 |- ( -. ( ph \/ ps ) -> -. ps )
3	1, 2	jca 306	. 2 |- ( -. ( ph \/ ps ) -> ( -. ph /\ -. ps ) )
4		simpl 109	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ph )
5	4	con2i 628	. . . 4 |- ( ph -> -. ( -. ph /\ -. ps ) )
6		simpr 110	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ps )
7	6	con2i 628	. . . 4 |- ( ps -> -. ( -. ph /\ -. ps ) )
8	5, 7	jaoi 718	. . 3 |- ( ( ph \/ ps ) -> -. ( -. ph /\ -. ps ) )
9	8	con2i 628	. 2 |- ( ( -. ph /\ -. ps ) -> -. ( ph \/ ps ) )
10	3, 9	impbii 126	1 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   \/ wo 710

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 615  ax-in2 616  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  782  nnexmid  852  dcor  938  3ioran  996  3ori  1313  unssdif  3416  difundi  3433  dcun  3578  sotricim  4388  sotritrieq  4390  en2lp  4620  poxp  6341  nntri2  6603  finexdc  7025  unfidisj  7045  fidcenumlemrks  7081  pw1nel3  7377  sucpw1nel3  7379  onntri45  7387  aptipr  7789  lttri3  8187  letr  8190  apirr  8713  apti  8730  elnnz  9417  xrlttri3  9954  xrletr  9965  exp3val  10723  bcval4  10934  hashunlem  10986  maxleast  11639  xrmaxlesup  11685  lcmval  12500  lcmcllem  12504  lcmgcdlem  12514  isprm3  12555  pcpremul  12731  ivthinc  15230  lgsdir2  15625  2lgslem3  15693  structiedg0val  15754  bj-nnor  15870  pwtrufal  16136  pwle2  16137