Theorem ioran 752

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 781, anordc 956, or ianordc 899. 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 738	. . 3 |- ( -. ( ph \/ ps ) -> -. ph )
2		pm2.46 739	. . 3 |- ( -. ( ph \/ ps ) -> -. ps )
3	1, 2	jca 306	. 2 |- ( -. ( ph \/ ps ) -> ( -. ph /\ -. ps ) )
4		simpl 109	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ph )
5	4	con2i 627	. . . 4 |- ( ph -> -. ( -. ph /\ -. ps ) )
6		simpr 110	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ps )
7	6	con2i 627	. . . 4 |- ( ps -> -. ( -. ph /\ -. ps ) )
8	5, 7	jaoi 716	. . 3 |- ( ( ph \/ ps ) -> -. ( -. ph /\ -. ps ) )
9	8	con2i 627	. 2 |- ( ( -. ph /\ -. ps ) -> -. ( ph \/ ps ) )
10	3, 9	impbii 126	1 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )

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

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 614  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  780  nnexmid  850  dcor  935  3ioran  993  3ori  1300  unssdif  3370  difundi  3387  dcun  3533  sotricim  4323  sotritrieq  4325  en2lp  4553  poxp  6232  nntri2  6494  finexdc  6901  unfidisj  6920  fidcenumlemrks  6951  pw1nel3  7229  sucpw1nel3  7231  onntri45  7239  aptipr  7639  lttri3  8036  letr  8039  apirr  8561  apti  8578  elnnz  9262  xrlttri3  9796  xrletr  9807  exp3val  10521  bcval4  10731  hashunlem  10783  maxleast  11221  xrmaxlesup  11266  lcmval  12062  lcmcllem  12066  lcmgcdlem  12076  isprm3  12117  pcpremul  12292  ivthinc  14091  lgsdir2  14404  bj-nnor  14456  pwtrufal  14717  pwle2  14718