![]() |
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 728 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | |
2 | pm1.4 728 | . 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | impbii 126 | 1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orcomd 730 orbi1i 764 orass 768 or32 771 or42 773 orbi1d 792 pm5.61 795 oranabs 816 ordir 818 pm2.1dc 838 notnotrdc 844 dcnnOLD 850 pm5.17dc 905 pm5.7dc 956 dn1dc 962 pm5.75 964 3orrot 986 3orcomb 989 excxor 1389 xorcom 1399 19.33b2 1640 nf4dc 1681 nf4r 1682 19.31r 1692 dveeq2 1826 sbequilem 1849 dvelimALT 2022 dvelimfv 2023 dvelimor 2030 eueq2dc 2925 uncom 3294 reuun2 3433 prel12 3786 exmid01 4213 exmidsssnc 4218 ordtriexmid 4535 ordtri2orexmid 4537 ontr2exmid 4539 onsucsssucexmid 4541 ordsoexmid 4576 ordtri2or2exmid 4585 cnvsom 5187 fununi 5299 frec0g 6416 frecabcl 6418 frecsuclem 6425 swoer 6581 inffiexmid 6924 exmidontriimlem1 7238 enq0tr 7451 letr 8058 reapmul1 8570 reapneg 8572 reapcotr 8573 remulext1 8574 apsym 8581 mulext1 8587 elznn0nn 9285 elznn0 9286 zapne 9345 nneoor 9373 nn01to3 9635 ltxr 9793 xrletr 9826 maxclpr 11249 minclpr 11263 odd2np1lem 11895 lcmcom 12082 dvdsprime 12140 coprm 12162 bdbl 14400 cos11 14671 lgsdir2lem4 14829 subctctexmid 15148 |
Copyright terms: Public domain | W3C validator |