Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orcom | Structured version Visualization version GIF version |
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.) |
Ref | Expression |
---|---|
orcom | ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm1.4 401 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | |
2 | pm1.4 401 | . 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | impbii 199 | 1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∨ wo 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 385 |
This theorem is referenced by: orcomd 403 orbi1i 542 orass 546 or32 549 or42 551 orbi1d 739 pm5.61 749 oranabs 901 ordir 909 pm5.17 932 pm5.7 975 pm5.75OLD 979 dn1 1008 dfifp7 1019 3orrot 1044 3orcomb 1048 cadan 1548 cadcomb 1552 nf2 1711 nfnbi 1781 19.31v 1870 19.31 2102 r19.30 3082 eueq2 3380 uncom 3757 undif3 3888 reuun2 3910 dfif2 4088 rabrsn 4259 tppreqb 4336 ssunsn2 4359 prel12 4383 disjor 4634 zfpair 4904 somin1 5529 ordtri2 5758 on0eqel 5845 fununi 5964 eliman0 6223 swoer 7772 supgtoreq 8376 cantnflem1d 8585 cantnflem1 8586 cflim2 9085 dffin7-2 9220 fpwwe2lem13 9464 suplem2pr 9875 leloe 10124 mulcan2g 10681 fimaxre 10968 arch 11289 elznn0nn 11391 elznn0 11392 nneo 11461 ltxr 11949 xrleloe 11977 xrrebnd 11999 xmullem2 12095 xmulcom 12096 xmulneg1 12099 xmulf 12102 sqeqori 12976 hashtpg 13267 odd2np1lem 15064 lcmcom 15306 dvdsprime 15400 coprm 15423 lvecvscan2 19112 opprdomn 19301 mplcoe1 19465 mplcoe5 19468 madutpos 20448 restntr 20986 alexsubALTlem2 21852 alexsubALTlem3 21853 xrsxmet 22612 dyaddisj 23364 mdegleb 23824 atandm3 24605 wilthlem2 24795 lgsdir2lem4 25053 tgcolg 25449 hlcomb 25498 axcontlem7 25850 nb3grprlem2 26283 vtxd0nedgb 26384 eupth2lem2 27079 eupth2lem3lem6 27093 hvmulcan2 27930 elat2 29199 chrelat2i 29224 atoml2i 29242 or3dir 29308 disjnf 29384 disjorf 29392 disjex 29405 disjexc 29406 disjunsn 29407 funcnv5mpt 29469 elicoelioo 29540 xrdifh 29542 tlt3 29665 orngsqr 29804 ballotlemfc0 30554 ballotlemfcc 30555 bnj563 30813 subfacp1lem6 31167 3orel2 31592 dfon2lem5 31692 noextenddif 31821 sleloe 31879 btwnconn1lem14 32207 outsideofcom 32235 outsideofeu 32238 lineunray 32254 ecase13d 32307 elicc3 32311 nn0prpw 32318 bj-dfbi5 32559 bj-consensusALT 32563 topdifinfeq 33198 onsucuni3 33215 wl-cases2-dnf 33295 itg2addnclem2 33462 itgaddnclem2 33469 orfa 33881 unitresl 33884 notornotel2 33898 tsbi4 33943 ineleq 34119 leatb 34579 leat2 34581 isat3 34594 hlrelat2 34689 elpadd0 35095 ifporcor 37806 ifpim2 37816 ifpim23g 37840 ifpim123g 37845 rp-fakeoranass 37859 elprn2 39866 stoweidlem26 40243 2reu3 41188 |
Copyright terms: Public domain | W3C validator |