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 850 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 846 |
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 847 |
This theorem is referenced by: pm2.25 889 biorf 936 3orel1 1092 xpcan 6008 funun 6385 sorpssuni 7476 sorpssint 7477 soxp 7849 ackbij1lem18 9737 ackbij1b 9739 fincssdom 9823 fin23lem30 9842 fin1a2lem13 9912 pythagtriplem4 16256 zringlpirlem3 20305 psgnodpm 20404 orngsqr 31080 elzdif0 31500 qqhval2lem 31501 eulerpartlemsv2 31895 eulerpartlemv 31901 eulerpartlemf 31907 eulerpartlemgh 31915 3orel13 33233 dfon2lem4 33334 dfon2lem6 33336 frxp3 33408 nosepdmlem 33527 dfrdg4 33891 rankeq1o 34111 wl-orel12 35293 poimirlem31 35431 pellfund14gap 40281 wepwsolem 40439 fmul01lt1lem1 42667 cncfiooicclem1 42976 etransclem24 43341 nnfoctbdjlem 43535 |
Copyright terms: Public domain | W3C validator |