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 1360 xorcom 1370 19.33b2 1609 nf4dc 1650 nf4r 1651 19.31r 1661 dveeq2 1795 sbequilem 1818 dvelimALT 1990 dvelimfv 1991 dvelimor 1998 eueq2dc 2885 uncom 3252 reuun2 3391 prel12 3736 exmid01 4162 exmidsssnc 4167 ordtriexmid 4483 ordtri2orexmid 4485 ontr2exmid 4487 onsucsssucexmid 4489 ordsoexmid 4524 ordtri2or2exmid 4533 cnvsom 5132 fununi 5241 frec0g 6347 frecabcl 6349 frecsuclem 6356 swoer 6511 inffiexmid 6854 exmidontriimlem1 7159 enq0tr 7357 letr 7963 reapmul1 8475 reapneg 8477 reapcotr 8478 remulext1 8479 apsym 8486 mulext1 8492 elznn0nn 9187 elznn0 9188 zapne 9244 nneoor 9272 nn01to3 9533 ltxr 9689 xrletr 9719 maxclpr 11134 minclpr 11148 odd2np1lem 11776 lcmcom 11957 dvdsprime 12015 coprm 12035 bdbl 12999 cos11 13270 subctctexmid 13670 |
Copyright terms: Public domain | W3C validator |