![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orcomd | Structured version Visualization version Unicode version |
Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.) |
Ref | Expression |
---|---|
orcomd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
orcomd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcomd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | orcom 393 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-or 376 |
This theorem is referenced by: olcd 399 19.33b 1752 swopo 4743 fr2nr 4790 ordtri1 5435 ssonprc 6607 ordunpr 6641 ordunisuc2 6659 2oconcl 7192 erdisj 7398 ordtypelem7 8026 ackbij1lem18 8654 fin23lem19 8753 gchi 9036 inar1 9187 inatsk 9190 avgle 10844 nnm1nn0 10901 uzsplit 11857 fzospliti 11943 fzouzsplit 11946 fz1f1o 13787 odcl 17196 odclOLD 17212 gexcl 17242 lssvs0or 18344 lspdisj 18359 lspsncv0 18380 mdetralt 19644 filcon 20909 limccnp 22858 dgrlt 23232 logreclem 23711 atans2 23869 basellem3 24021 sqff1o 24121 tgcgrsub2 24652 legov3 24655 colline 24706 tglowdim2ln 24708 mirbtwnhl 24737 colmid 24745 symquadlem 24746 midexlem 24749 ragperp 24774 colperp 24783 midex 24791 oppperpex 24807 hlpasch 24810 colopp 24823 colhp 24824 lmieu 24838 lmicom 24842 lmimid 24848 lmiisolem 24850 trgcopy 24858 cgracgr 24872 cgraswap 24874 cgracol 24881 hashecclwwlkn1 25574 znsqcld 28331 xlt2addrd 28346 esumcvgre 28919 eulerpartlemgvv 29215 nobndup 30595 ordtoplem 31101 ordcmp 31113 onsucuni3 31772 dvasin 32030 unitresr 32321 lkrshp4 32676 2at0mat0 33092 trlator0 33739 dia2dimlem2 34635 dia2dimlem3 34636 dochkrshp 34956 dochkrshp4 34959 lcfl6 35070 lclkrlem2k 35087 hdmap14lem6 35446 hgmapval0 35465 acongneg2 35829 unxpwdom3 35955 elunnel2 37357 disjinfi 37478 xrssre 37602 icccncfext 37807 wallispilem3 37986 fourierdlem93 38120 fourierdlem101 38128 nneop 40658 |
Copyright terms: Public domain | W3C validator |