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 848 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 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 206 df-or 845 |
This theorem is referenced by: pm2.25 887 biorf 934 3orel1 1090 xpcan 6079 funun 6480 sorpssuni 7585 sorpssint 7586 soxp 7970 ackbij1lem18 9993 ackbij1b 9995 fincssdom 10079 fin23lem30 10098 fin1a2lem13 10168 pythagtriplem4 16520 zringlpirlem3 20686 psgnodpm 20793 orngsqr 31503 elzdif0 31930 qqhval2lem 31931 eulerpartlemsv2 32325 eulerpartlemv 32331 eulerpartlemf 32337 eulerpartlemgh 32345 3orel13 33660 dfon2lem4 33762 dfon2lem6 33764 frxp3 33797 nosepdmlem 33886 dfrdg4 34253 rankeq1o 34473 wl-orel12 35670 poimirlem31 35808 pellfund14gap 40709 wepwsolem 40867 fmul01lt1lem1 43125 cncfiooicclem1 43434 etransclem24 43799 nnfoctbdjlem 43993 |
Copyright terms: Public domain | W3C validator |