Theorem ioran 753

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 782, anordc 958, or ianordc 900. 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 739	. . 3 |- ( -. ( ph \/ ps ) -> -. ph )
2		pm2.46 740	. . 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 717	. . 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 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.56  781  nnexmid  851  dcor  937  3ioran  995  3ori  1311  unssdif  3394  difundi  3411  dcun  3556  sotricim  4354  sotritrieq  4356  en2lp  4586  poxp  6285  nntri2  6547  finexdc  6958  unfidisj  6978  fidcenumlemrks  7012  pw1nel3  7291  sucpw1nel3  7293  onntri45  7301  aptipr  7701  lttri3  8099  letr  8102  apirr  8624  apti  8641  elnnz  9327  xrlttri3  9863  xrletr  9874  exp3val  10612  bcval4  10823  hashunlem  10875  maxleast  11357  xrmaxlesup  11402  lcmval  12201  lcmcllem  12205  lcmgcdlem  12215  isprm3  12256  pcpremul  12431  ivthinc  14797  lgsdir2  15149  bj-nnor  15226  pwtrufal  15488  pwle2  15489