![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orel1 | Structured version Visualization version GIF version |
Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.) |
Ref | Expression |
---|---|
orel1 | ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.53 387 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 |
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 |
This theorem is referenced by: pm2.25 418 biorf 419 3orel1 1076 prel12OLD 4527 xpcan 5728 funun 6093 sorpssuni 7112 sorpssint 7113 soxp 7459 ackbij1lem18 9271 ackbij1b 9273 fincssdom 9357 fin23lem30 9376 fin1a2lem13 9446 pythagtriplem4 15746 evlslem3 19736 zringlpirlem3 20056 psgnodpm 20156 orngsqr 30134 elzdif0 30354 qqhval2lem 30355 eulerpartlemsv2 30750 eulerpartlemv 30756 eulerpartlemf 30762 eulerpartlemgh 30770 3orel13 31926 dfon2lem4 32017 dfon2lem6 32019 nosepdmlem 32160 dfrdg4 32385 rankeq1o 32605 wl-orel12 33625 poimirlem31 33771 pellfund14gap 37971 wepwsolem 38132 fmul01lt1lem1 40337 cncfiooicclem1 40627 etransclem24 40996 nnfoctbdjlem 41193 |
Copyright terms: Public domain | W3C validator |