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 722 | . 2 | |
2 | pm1.4 722 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 703 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orcomd 724 orbi1i 758 orass 762 or32 765 or42 767 orbi1d 786 pm5.61 789 oranabs 810 ordir 812 pm2.1dc 832 notnotrdc 838 dcnnOLD 844 pm5.17dc 899 pm5.7dc 949 dn1dc 955 pm5.75 957 3orrot 979 3orcomb 982 excxor 1373 xorcom 1383 19.33b2 1622 nf4dc 1663 nf4r 1664 19.31r 1674 dveeq2 1808 sbequilem 1831 dvelimALT 2003 dvelimfv 2004 dvelimor 2011 eueq2dc 2903 uncom 3271 reuun2 3410 prel12 3758 exmid01 4184 exmidsssnc 4189 ordtriexmid 4505 ordtri2orexmid 4507 ontr2exmid 4509 onsucsssucexmid 4511 ordsoexmid 4546 ordtri2or2exmid 4555 cnvsom 5154 fununi 5266 frec0g 6376 frecabcl 6378 frecsuclem 6385 swoer 6541 inffiexmid 6884 exmidontriimlem1 7198 enq0tr 7396 letr 8002 reapmul1 8514 reapneg 8516 reapcotr 8517 remulext1 8518 apsym 8525 mulext1 8531 elznn0nn 9226 elznn0 9227 zapne 9286 nneoor 9314 nn01to3 9576 ltxr 9732 xrletr 9765 maxclpr 11186 minclpr 11200 odd2np1lem 11831 lcmcom 12018 dvdsprime 12076 coprm 12098 bdbl 13297 cos11 13568 lgsdir2lem4 13726 subctctexmid 14034 |
Copyright terms: Public domain | W3C validator |