![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orcom | GIF 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 682 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | |
2 | pm1.4 682 | . 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 665 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orcomd 684 orbi1i 716 orass 720 or32 723 or42 725 orbi1d 741 pm5.61 744 oranabs 765 ordir 767 pm2.1dc 784 notnotrdc 790 pm5.17dc 849 testbitestn 862 pm5.7dc 901 dn1dc 907 pm5.75 909 3orrot 931 3orcomb 934 excxor 1315 xorcom 1325 19.33b2 1566 nf4dc 1606 nf4r 1607 19.31r 1617 dveeq2 1744 sbequilem 1767 dvelimALT 1935 dvelimfv 1936 dvelimor 1943 eueq2dc 2789 uncom 3145 reuun2 3283 prel12 3621 exmid01 4038 ordtriexmid 4351 ordtri2orexmid 4352 ontr2exmid 4354 onsucsssucexmid 4356 ordsoexmid 4391 ordtri2or2exmid 4400 cnvsom 4987 fununi 5095 frec0g 6176 frecabcl 6178 frecsuclem 6185 swoer 6334 inffiexmid 6676 enq0tr 7054 letr 7629 reapmul1 8133 reapneg 8135 reapcotr 8136 remulext1 8137 apsym 8144 mulext1 8150 elznn0nn 8825 elznn0 8826 zapne 8882 nneoor 8909 nn01to3 9163 ltxr 9307 xrletr 9334 maxclpr 10716 odd2np1lem 11211 lcmcom 11385 dvdsprime 11443 coprm 11462 |
Copyright terms: Public domain | W3C validator |