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  3408  difundi  3425  dcun  3570  sotricim  4370  sotritrieq  4372  en2lp  4602  poxp  6318  nntri2  6580  finexdc  6999  unfidisj  7019  fidcenumlemrks  7055  pw1nel3  7343  sucpw1nel3  7345  onntri45  7353  aptipr  7754  lttri3  8152  letr  8155  apirr  8678  apti  8695  elnnz  9382  xrlttri3  9919  xrletr  9930  exp3val  10686  bcval4  10897  hashunlem  10949  maxleast  11524  xrmaxlesup  11570  lcmval  12385  lcmcllem  12389  lcmgcdlem  12399  isprm3  12440  pcpremul  12616  ivthinc  15115  lgsdir2  15510  2lgslem3  15578  structiedg0val  15637  bj-nnor  15670  pwtrufal  15934  pwle2  15935