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 646 | . 2 | |
2 | pm1.4 646 | . 2 | |
3 | 1, 2 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orcomd 648 orbi1i 680 orass 684 or32 687 or42 689 orbi1d 705 pm5.61 708 oranabs 728 ordir 730 pm2.1dc 745 notnotrdc 751 pm5.17dc 810 testbitestn 823 pm5.7dc 861 dn1dc 867 pm5.75 869 3orrot 891 3orcomb 894 excxor 1269 xorcom 1279 19.33b2 1520 nf4dc 1560 nf4r 1561 19.31r 1571 dveeq2 1696 sbequilem 1719 dvelimALT 1886 dvelimfv 1887 dvelimor 1894 eueq2dc 2714 uncom 3087 reuun2 3220 prel12 3542 ordtriexmid 4247 ordtri2orexmid 4248 ontr2exmid 4250 onsucsssucexmid 4252 ordsoexmid 4286 ordtri2or2exmid 4296 cnvsom 4861 fununi 4967 frec0g 5983 frecsuclem3 5990 swoer 6134 enq0tr 6532 letr 7101 reapmul1 7586 reapneg 7588 reapcotr 7589 remulext1 7590 apsym 7597 mulext1 7603 elznn0nn 8259 elznn0 8260 zapne 8315 nneoor 8340 nn01to3 8552 ltxr 8695 xrletr 8724 |
Copyright terms: Public domain | W3C validator |