![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orcom | Unicode version |
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.) |
Ref | Expression |
---|---|
orcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm1.4 727 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm1.4 727 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orcomd 729 orbi1i 763 orass 767 or32 770 or42 772 orbi1d 791 pm5.61 794 oranabs 815 ordir 817 pm2.1dc 837 notnotrdc 843 dcnnOLD 849 pm5.17dc 904 pm5.7dc 954 dn1dc 960 pm5.75 962 3orrot 984 3orcomb 987 excxor 1378 xorcom 1388 19.33b2 1629 nf4dc 1670 nf4r 1671 19.31r 1681 dveeq2 1815 sbequilem 1838 dvelimALT 2010 dvelimfv 2011 dvelimor 2018 eueq2dc 2910 uncom 3279 reuun2 3418 prel12 3771 exmid01 4198 exmidsssnc 4203 ordtriexmid 4520 ordtri2orexmid 4522 ontr2exmid 4524 onsucsssucexmid 4526 ordsoexmid 4561 ordtri2or2exmid 4570 cnvsom 5172 fununi 5284 frec0g 6397 frecabcl 6399 frecsuclem 6406 swoer 6562 inffiexmid 6905 exmidontriimlem1 7219 enq0tr 7432 letr 8038 reapmul1 8550 reapneg 8552 reapcotr 8553 remulext1 8554 apsym 8561 mulext1 8567 elznn0nn 9265 elznn0 9266 zapne 9325 nneoor 9353 nn01to3 9615 ltxr 9773 xrletr 9806 maxclpr 11226 minclpr 11240 odd2np1lem 11871 lcmcom 12058 dvdsprime 12116 coprm 12138 bdbl 13896 cos11 14167 lgsdir2lem4 14325 subctctexmid 14632 |
Copyright terms: Public domain | W3C validator |