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 388 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 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 385 |
This theorem is referenced by: pm2.25 419 biorf 420 3orel1 1041 prel12 4383 xpcan 5570 funun 5932 sorpssuni 6946 sorpssint 6947 soxp 7290 ackbij1lem18 9059 ackbij1b 9061 fincssdom 9145 fin23lem30 9164 fin1a2lem13 9234 pythagtriplem4 15524 evlslem3 19514 zringlpirlem3 19834 psgnodpm 19934 orngsqr 29804 elzdif0 30024 qqhval2lem 30025 eulerpartlemsv2 30420 eulerpartlemv 30426 eulerpartlemf 30432 eulerpartlemgh 30440 3orel13 31598 dfon2lem4 31691 dfon2lem6 31693 nosepdmlem 31833 dfrdg4 32058 rankeq1o 32278 wl-orel12 33294 poimirlem31 33440 pellfund14gap 37451 wepwsolem 37612 fmul01lt1lem1 39816 cncfiooicclem1 40106 etransclem24 40475 nnfoctbdjlem 40672 |
Copyright terms: Public domain | W3C validator |