![]() |
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 717 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | |
2 | pm1.4 717 | . 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orcomd 719 orbi1i 753 orass 757 or32 760 or42 762 orbi1d 781 pm5.61 784 oranabs 805 ordir 807 pm2.1dc 823 notnotrdc 829 dcnnOLD 835 pm5.17dc 890 pm5.7dc 939 dn1dc 945 pm5.75 947 3orrot 969 3orcomb 972 excxor 1357 xorcom 1367 19.33b2 1609 nf4dc 1649 nf4r 1650 19.31r 1660 dveeq2 1788 sbequilem 1811 dvelimALT 1986 dvelimfv 1987 dvelimor 1994 eueq2dc 2861 uncom 3225 reuun2 3364 prel12 3706 exmid01 4129 exmidsssnc 4134 ordtriexmid 4445 ordtri2orexmid 4446 ontr2exmid 4448 onsucsssucexmid 4450 ordsoexmid 4485 ordtri2or2exmid 4494 cnvsom 5090 fununi 5199 frec0g 6302 frecabcl 6304 frecsuclem 6311 swoer 6465 inffiexmid 6808 enq0tr 7266 letr 7871 reapmul1 8381 reapneg 8383 reapcotr 8384 remulext1 8385 apsym 8392 mulext1 8398 elznn0nn 9092 elznn0 9093 zapne 9149 nneoor 9177 nn01to3 9436 ltxr 9592 xrletr 9621 maxclpr 11026 minclpr 11040 odd2np1lem 11605 lcmcom 11781 dvdsprime 11839 coprm 11858 bdbl 12711 cos11 12982 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |