Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orel2 | Structured version Visualization version GIF version |
Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.) |
Ref | Expression |
---|---|
orel2 | ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 24 | . 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜓)) | |
2 | pm2.21 123 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
3 | 1, 2 | jaod 855 | 1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 |
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 209 df-or 844 |
This theorem is referenced by: pm2.64 938 pm2.74 971 pm5.61 997 pm5.71 1024 xpcan2 6036 funun 6402 fnpr2ob 16833 ablfac1eulem 19196 drngmuleq0 19527 mdetunilem9 21231 maducoeval2 21251 tdeglem4 24656 deg1sublt 24706 dgrnznn 24839 dvply1 24875 aaliou2 24931 colline 26437 axcontlem2 26753 3orel3 32944 dfrdg4 33414 arg-ax 33766 unbdqndv2lem2 33851 elpell14qr2 39466 elpell1qr2 39476 jm2.22 39599 jm2.23 39600 jm2.26lem3 39605 ttac 39640 wepwsolem 39649 3ornot23VD 41188 fmul01lt1lem2 41873 cncfiooicclem1 42183 |
Copyright terms: Public domain | W3C validator |