![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orel2 | Structured version Visualization version Unicode 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 25 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.21 112 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jaod 382 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-or 372 |
This theorem is referenced by: biorfi 409 pm2.64 798 pm2.74 857 pm5.71 947 prel12 4152 xpcan2 5274 funun 5624 ablfac1eulem 17705 drngmuleq0 17998 mdetunilem9 19645 maducoeval2 19665 tdeglem4 23009 deg1sublt 23059 dgrnznn 23201 dvply1 23237 aaliou2 23296 colline 24694 axcontlem2 24995 3orel3 30344 dfrdg4 30718 arg-ax 31076 elpell14qr2 35708 elpell1qr2 35718 jm2.22 35850 jm2.23 35851 jm2.26lem3 35856 ttac 35891 wepwsolem 35900 3ornot23VD 37243 fmul01lt1lem2 37663 cncfiooicclem1 37771 |
Copyright terms: Public domain | W3C validator |