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 717 | . 2 | |
2 | pm1.4 717 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 698 |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orcomd 719 orbi1i 753 orass 757 or32 760 or42 762 orbi1d 781 pm5.61 784 oranabs 805 ordir 807 pm2.1dc 823 notnotrdc 829 dcnnOLD 835 pm5.17dc 890 pm5.7dc 939 dn1dc 945 pm5.75 947 3orrot 969 3orcomb 972 excxor 1360 xorcom 1370 19.33b2 1609 nf4dc 1650 nf4r 1651 19.31r 1661 dveeq2 1795 sbequilem 1818 dvelimALT 1990 dvelimfv 1991 dvelimor 1998 eueq2dc 2885 uncom 3251 reuun2 3390 prel12 3734 exmid01 4159 exmidsssnc 4164 ordtriexmid 4480 ordtri2orexmid 4482 ontr2exmid 4484 onsucsssucexmid 4486 ordsoexmid 4521 ordtri2or2exmid 4530 cnvsom 5129 fununi 5238 frec0g 6344 frecabcl 6346 frecsuclem 6353 swoer 6508 inffiexmid 6851 exmidontriimlem1 7156 enq0tr 7354 letr 7960 reapmul1 8470 reapneg 8472 reapcotr 8473 remulext1 8474 apsym 8481 mulext1 8487 elznn0nn 9181 elznn0 9182 zapne 9238 nneoor 9266 nn01to3 9526 ltxr 9682 xrletr 9712 maxclpr 11122 minclpr 11136 odd2np1lem 11762 lcmcom 11940 dvdsprime 11998 coprm 12018 bdbl 12903 cos11 13174 subctctexmid 13573 |
Copyright terms: Public domain | W3C validator |