Theorem ioran 757

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 786, anordc 962, or ianordc 904. 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 743	. . 3 |- ( -. ( ph \/ ps ) -> -. ph )
2		pm2.46 744	. . 3 |- ( -. ( ph \/ ps ) -> -. ps )
3	1, 2	jca 306	. 2 |- ( -. ( ph \/ ps ) -> ( -. ph /\ -. ps ) )
4		simpl 109	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ph )
5	4	con2i 630	. . . 4 |- ( ph -> -. ( -. ph /\ -. ps ) )
6		simpr 110	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ps )
7	6	con2i 630	. . . 4 |- ( ps -> -. ( -. ph /\ -. ps ) )
8	5, 7	jaoi 721	. . 3 |- ( ( ph \/ ps ) -> -. ( -. ph /\ -. ps ) )
9	8	con2i 630	. 2 |- ( ( -. ph /\ -. ps ) -> -. ( ph \/ ps ) )
10	3, 9	impbii 126	1 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )

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

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 617  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  785  nnexmid  855  dcor  941  3ioran  1017  3ori  1334  ecase2d  1385  unssdif  3439  difundi  3456  dcun  3601  sotricim  4414  sotritrieq  4416  en2lp  4646  poxp  6378  nntri2  6640  finexdc  7064  unfidisj  7084  fidcenumlemrks  7120  pw1nel3  7416  sucpw1nel3  7418  onntri45  7426  aptipr  7828  lttri3  8226  letr  8229  apirr  8752  apti  8769  elnnz  9456  xrlttri3  9993  xrletr  10004  exp3val  10763  bcval4  10974  hashunlem  11026  maxleast  11724  xrmaxlesup  11770  lcmval  12585  lcmcllem  12589  lcmgcdlem  12599  isprm3  12640  pcpremul  12816  ivthinc  15317  lgsdir2  15712  2lgslem3  15780  structiedg0val  15841  bj-nnor  16098  pwtrufal  16363  pwle2  16364