Theorem ioran 742

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 771, anordc 946, or ianordc 889. 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 728	. . 3 |- ( -. ( ph \/ ps ) -> -. ph )
2		pm2.46 729	. . 3 |- ( -. ( ph \/ ps ) -> -. ps )
3	1, 2	jca 304	. 2 |- ( -. ( ph \/ ps ) -> ( -. ph /\ -. ps ) )
4		simpl 108	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ph )
5	4	con2i 617	. . . 4 |- ( ph -> -. ( -. ph /\ -. ps ) )
6		simpr 109	. . . . 5 |- ( ( -. ph /\ -. ps ) -> -. ps )
7	6	con2i 617	. . . 4 |- ( ps -> -. ( -. ph /\ -. ps ) )
8	5, 7	jaoi 706	. . 3 |- ( ( ph \/ ps ) -> -. ( -. ph /\ -. ps ) )
9	8	con2i 617	. 2 |- ( ( -. ph /\ -. ps ) -> -. ( ph \/ ps ) )
10	3, 9	impbii 125	1 |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )

Syntax hints:   -. wn 3   /\ wa 103   <-> wb 104   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.56  770  nnexmid  840  dcor  925  3ioran  983  3ori  1290  unssdif  3357  difundi  3374  dcun  3519  sotricim  4301  sotritrieq  4303  en2lp  4531  poxp  6200  nntri2  6462  finexdc  6868  unfidisj  6887  fidcenumlemrks  6918  pw1nel3  7187  sucpw1nel3  7189  onntri45  7197  aptipr  7582  lttri3  7978  letr  7981  apirr  8503  apti  8520  elnnz  9201  xrlttri3  9733  xrletr  9744  exp3val  10457  bcval4  10665  hashunlem  10717  maxleast  11155  xrmaxlesup  11200  lcmval  11995  lcmcllem  11999  lcmgcdlem  12009  isprm3  12050  pcpremul  12225  ivthinc  13261  lgsdir2  13574  bj-nnor  13615  pwtrufal  13877  pwle2  13878