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  4371  sotritrieq  4373  en2lp  4603  poxp  6320  nntri2  6582  finexdc  7001  unfidisj  7021  fidcenumlemrks  7057  pw1nel3  7345  sucpw1nel3  7347  onntri45  7355  aptipr  7756  lttri3  8154  letr  8157  apirr  8680  apti  8697  elnnz  9384  xrlttri3  9921  xrletr  9932  exp3val  10688  bcval4  10899  hashunlem  10951  maxleast  11557  xrmaxlesup  11603  lcmval  12418  lcmcllem  12422  lcmgcdlem  12432  isprm3  12473  pcpremul  12649  ivthinc  15148  lgsdir2  15543  2lgslem3  15611  structiedg0val  15670  bj-nnor  15707  pwtrufal  15971  pwle2  15972