![]() |
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 856 | 1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 844 |
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 210 df-or 845 |
This theorem is referenced by: pm2.64 939 pm2.74 972 pm5.61 998 pm5.71 1025 xpcan2 6001 funun 6370 fnpr2ob 16823 ablfac1eulem 19187 drngmuleq0 19518 mdetunilem9 21225 maducoeval2 21245 tdeglem4 24661 deg1sublt 24711 dgrnznn 24844 dvply1 24880 aaliou2 24936 colline 26443 axcontlem2 26759 3orel3 33055 dfrdg4 33525 arg-ax 33877 unbdqndv2lem2 33962 elpell14qr2 39803 elpell1qr2 39813 jm2.22 39936 jm2.23 39937 jm2.26lem3 39942 ttac 39977 wepwsolem 39986 3ornot23VD 41553 fmul01lt1lem2 42227 cncfiooicclem1 42535 |
Copyright terms: Public domain | W3C validator |