![]() |
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 878 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 874 |
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 199 df-or 875 |
This theorem is referenced by: pm2.25 914 biorf 961 3orel1 1112 prel12OLD 4568 xpcan 5787 funun 6146 sorpssuni 7180 sorpssint 7181 soxp 7527 ackbij1lem18 9347 ackbij1b 9349 fincssdom 9433 fin23lem30 9452 fin1a2lem13 9522 pythagtriplem4 15857 evlslem3 19836 zringlpirlem3 20156 psgnodpm 20255 orngsqr 30320 elzdif0 30540 qqhval2lem 30541 eulerpartlemsv2 30936 eulerpartlemv 30942 eulerpartlemf 30948 eulerpartlemgh 30956 3orel13 32113 dfon2lem4 32203 dfon2lem6 32205 nosepdmlem 32346 dfrdg4 32571 rankeq1o 32791 wl-orel12 33792 poimirlem31 33929 pellfund14gap 38233 wepwsolem 38393 fmul01lt1lem1 40556 cncfiooicclem1 40846 etransclem24 41214 nnfoctbdjlem 41411 |
Copyright terms: Public domain | W3C validator |