![]() |
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 645 | . 2 ⊢ ((φ ∨ ψ) → (ψ ∨ φ)) | |
2 | pm1.4 645 | . 2 ⊢ ((ψ ∨ φ) → (φ ∨ ψ)) | |
3 | 1, 2 | impbii 117 | 1 ⊢ ((φ ∨ ψ) ↔ (ψ ∨ φ)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∨ wo 628 |
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 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orcomd 647 orbi1i 679 orass 683 or32 686 or42 688 orbi1d 704 pm5.61 707 oranabs 727 ordir 729 pm2.1dc 744 notnot2dc 750 pm5.17dc 809 testbitestn 822 pm5.7dc 860 dn1dc 866 pm5.75 868 3orrot 890 3orcomb 893 excxor 1268 xorcom 1276 19.33b2 1517 nf4dc 1557 nf4r 1558 19.31r 1568 dveeq2 1693 sbequilem 1716 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 eueq2dc 2708 uncom 3081 reuun2 3214 prel12 3533 ordtriexmid 4210 ordtri2orexmid 4211 onsucsssucexmid 4212 ordsoexmid 4240 cnvsom 4804 fununi 4910 frec0g 5922 frecsuclem3 5929 swoer 6070 enq0tr 6417 letr 6898 reapmul1 7379 reapneg 7381 reapcotr 7382 remulext1 7383 apsym 7390 mulext1 7396 elznn0nn 8035 elznn0 8036 zapne 8091 nneoor 8116 nn01to3 8328 ltxr 8465 xrletr 8494 |
Copyright terms: Public domain | W3C validator |