![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm4.56 | Structured version Visualization version GIF version |
Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm4.56 | ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioran 512 | . 2 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | bicomi 214 | 1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∨ wo 382 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 |
This theorem is referenced by: oran 518 neanior 3016 prneimg 4524 ordtri3OLD 5913 ssxr 10291 isirred2 18893 aaliou3lem9 24296 mideulem2 25817 opphllem 25818 bj-dfbi4 32856 topdifinffinlem 33498 icorempt2 33502 dalawlem13 35664 cdleme22b 36123 jm2.26lem3 38062 wopprc 38091 iunconnlem2 39662 icccncfext 40595 cncfiooicc 40602 fourierdlem25 40844 fourierdlem35 40854 fourierswlem 40942 fouriersw 40943 etransclem44 40990 sge0split 41121 islininds2 42775 digexp 42903 |
Copyright terms: Public domain | W3C validator |