![]() |
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 3024 prneimg 4532 ordtri3OLD 5921 ssxr 10319 isirred2 18921 aaliou3lem9 24324 mideulem2 25846 opphllem 25847 bj-dfbi4 32886 topdifinffinlem 33524 icorempt2 33528 dalawlem13 35690 cdleme22b 36149 jm2.26lem3 38088 wopprc 38117 iunconnlem2 39688 icccncfext 40621 cncfiooicc 40628 fourierdlem25 40870 fourierdlem35 40880 fourierswlem 40968 fouriersw 40969 etransclem44 41016 sge0split 41147 islininds2 42801 digexp 42929 |
Copyright terms: Public domain | W3C validator |