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 701 | . 2 | |
2 | pm1.4 701 | . 2 | |
3 | 1, 2 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 682 |
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 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orcomd 703 orbi1i 737 orass 741 or32 744 or42 746 orbi1d 765 pm5.61 768 oranabs 789 ordir 791 pm2.1dc 807 notnotrdc 813 dcnnOLD 819 pm5.17dc 874 pm5.7dc 923 dn1dc 929 pm5.75 931 3orrot 953 3orcomb 956 excxor 1341 xorcom 1351 19.33b2 1593 nf4dc 1633 nf4r 1634 19.31r 1644 dveeq2 1771 sbequilem 1794 dvelimALT 1963 dvelimfv 1964 dvelimor 1971 eueq2dc 2830 uncom 3190 reuun2 3329 prel12 3668 exmid01 4091 exmidsssnc 4096 ordtriexmid 4407 ordtri2orexmid 4408 ontr2exmid 4410 onsucsssucexmid 4412 ordsoexmid 4447 ordtri2or2exmid 4456 cnvsom 5052 fununi 5161 frec0g 6262 frecabcl 6264 frecsuclem 6271 swoer 6425 inffiexmid 6768 enq0tr 7210 letr 7815 reapmul1 8324 reapneg 8326 reapcotr 8327 remulext1 8328 apsym 8335 mulext1 8341 elznn0nn 9026 elznn0 9027 zapne 9083 nneoor 9111 nn01to3 9365 ltxr 9517 xrletr 9546 maxclpr 10949 minclpr 10963 odd2np1lem 11481 lcmcom 11657 dvdsprime 11715 coprm 11734 bdbl 12583 subctctexmid 13092 |
Copyright terms: Public domain | W3C validator |