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 510 | . 2 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | bicomi 213 | 1 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 ∨ 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 196 df-or 384 df-an 385 |
This theorem is referenced by: oran 516 neanior 2874 prneimg 4328 ordtri3OLD 5677 ssxr 9986 isirred2 18524 aaliou3lem9 23909 mideulem2 25426 opphllem 25427 bj-dfbi4 31728 topdifinffinlem 32371 icorempt2 32375 dalawlem13 34187 cdleme22b 34647 jm2.26lem3 36586 wopprc 36615 iunconlem2 38193 icccncfext 38773 cncfiooicc 38780 fourierdlem25 39025 fourierdlem35 39035 fourierswlem 39123 fouriersw 39124 etransclem44 39171 sge0split 39302 islininds2 42067 digexp 42199 |
Copyright terms: Public domain | W3C validator |