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 400 | . 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑)) | |
2 | pm1.4 400 | . 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓)) | |
3 | 1, 2 | impbii 198 | 1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∨ wo 382 |
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 196 df-or 384 |
This theorem is referenced by: orcomd 402 orbi1i 541 orass 545 or32 548 or42 550 orbi1d 735 pm5.61 745 oranabs 897 ordir 905 pm5.17 928 pm5.7 971 pm5.75OLD 975 dn1 1000 dfifp7 1013 3orrot 1037 3orcomb 1041 cadan 1539 cadcomb 1543 nf2 1702 19.31v 1857 19.31 2089 r19.30 3063 eueq2 3347 uncom 3719 undif3 3847 reuun2 3869 dfif2 4038 rabrsn 4203 tppreqb 4277 ssunsn2 4299 prel12 4323 disjor 4567 zfpair 4831 somin1 5448 ordtri2 5675 on0eqel 5762 fununi 5878 eliman0 6133 swoer 7659 supgtoreq 8259 cantnflem1d 8468 cantnflem1 8469 cflim2 8968 dffin7-2 9103 fpwwe2lem13 9343 suplem2pr 9754 leloe 10003 mulcan2g 10560 fimaxre 10847 arch 11166 elznn0nn 11268 elznn0 11269 nneo 11337 ltxr 11825 xrleloe 11853 xrrebnd 11873 xmullem2 11967 xmulcom 11968 xmulneg1 11971 xmulf 11974 sqeqori 12838 hashtpg 13121 odd2np1lem 14902 lcmcom 15144 dvdsprime 15238 coprm 15261 lvecvscan2 18933 opprdomn 19122 mplcoe1 19286 mplcoe5 19289 madutpos 20267 restntr 20796 alexsubALTlem2 21662 alexsubALTlem3 21663 xrsxmet 22420 dyaddisj 23170 mdegleb 23628 atandm3 24405 wilthlem2 24595 lgsdir2lem4 24853 tgcolg 25249 hlcomb 25298 axcontlem7 25650 nb3graprlem2 25981 eupath2lem2 26505 eupath2lem3 26506 hvmulcan2 27314 elat2 28583 chrelat2i 28608 atoml2i 28626 or3dir 28692 disjnf 28766 disjorf 28774 disjex 28787 disjexc 28788 disjunsn 28789 funcnv5mpt 28852 elicoelioo 28930 xrdifh 28932 tlt3 28996 orngsqr 29135 ballotlemfc0 29881 ballotlemfcc 29882 bnj563 30067 subfacp1lem6 30421 3orel2 30847 socnv 30908 dfon2lem5 30936 btwnconn1lem14 31377 outsideofcom 31405 outsideofeu 31408 lineunray 31424 ecase13d 31477 elicc3 31481 nn0prpw 31488 bj-dfbi5 31729 bj-consensusALT 31733 bj-nf2 31766 bj-nfn 31795 topdifinfeq 32374 onsucuni3 32391 wl-cases2-dnf 32474 itg2addnclem2 32632 itgaddnclem2 32639 orfa 33051 unitresl 33054 notornotel2 33068 tsbi4 33113 leatb 33597 leat2 33599 isat3 33612 hlrelat2 33707 elpadd0 34113 ifporcor 36825 ifpim2 36835 ifpim23g 36859 ifpim123g 36864 rp-fakeoranass 36878 elprn2 38701 stoweidlem26 38919 2reu3 39837 nb3grprlem2 40609 vtxd0nedgb 40703 eupth2lem2 41387 eupth2lem3lem6 41401 |
Copyright terms: Public domain | W3C validator |