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	⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		pm2.45 740	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
2		pm2.46 741	. . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
3	1, 2	jca 306	. 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓))
4		simpl 109	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑)
5	4	con2i 628	. . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
6		simpr 110	. . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓)
7	6	con2i 628	. . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
8	5, 7	jaoi 718	. . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓))
9	8	con2i 628	. 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓))
10	3, 9	impbii 126	1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))

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  3412  difundi  3429  dcun  3574  sotricim  4378  sotritrieq  4380  en2lp  4610  poxp  6331  nntri2  6593  finexdc  7014  unfidisj  7034  fidcenumlemrks  7070  pw1nel3  7362  sucpw1nel3  7364  onntri45  7372  aptipr  7774  lttri3  8172  letr  8175  apirr  8698  apti  8715  elnnz  9402  xrlttri3  9939  xrletr  9950  exp3val  10708  bcval4  10919  hashunlem  10971  maxleast  11599  xrmaxlesup  11645  lcmval  12460  lcmcllem  12464  lcmgcdlem  12474  isprm3  12515  pcpremul  12691  ivthinc  15190  lgsdir2  15585  2lgslem3  15653  structiedg0val  15714  bj-nnor  15809  pwtrufal  16075  pwle2  16076