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 196 df-or 384 |
This theorem is referenced by: pm2.25 418 biorf 419 prel12 4323 xpcan 5489 funun 5846 sorpssuni 6844 sorpssint 6845 soxp 7177 ackbij1lem18 8942 ackbij1b 8944 fincssdom 9028 fin23lem30 9047 fin1a2lem13 9117 pythagtriplem4 15362 evlslem3 19335 zringlpirlem3 19653 psgnodpm 19753 orngsqr 29135 elzdif0 29352 qqhval2lem 29353 eulerpartlemsv2 29747 eulerpartlemv 29753 eulerpartlemf 29759 eulerpartlemgh 29767 3orel1 30846 3orel13 30853 dfon2lem4 30935 dfon2lem6 30937 dfrdg4 31228 rankeq1o 31448 wl-orel12 32473 poimirlem31 32610 pellfund14gap 36469 wepwsolem 36630 fmul01lt1lem1 38651 cncfiooicclem1 38779 etransclem24 39151 nnfoctbdjlem 39348 |
Copyright terms: Public domain | W3C validator |