![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > orcomd | Structured 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 387 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 196 |
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 185 df-or 370 |
This theorem is referenced by: olcd 393 19.33b 1664 swopo 4751 fr2nr 4798 ordtri1 4852 ssonprc 6505 ordunpr 6539 ordunisuc2 6557 2oconcl 7045 erdisj 7250 ordtypelem7 7841 ackbij1lem18 8509 fin23lem19 8608 gchi 8894 inar1 9045 inatsk 9048 avgle 10669 nnm1nn0 10724 uzsplit 11633 fzm1 11643 fzospliti 11684 fzouzsplit 11687 fz1f1o 13291 odcl 16145 gexcl 16185 lssvs0or 17299 lspdisj 17314 lspsncv0 17335 mdetralt 18532 filcon 19574 limccnp 21484 dgrlt 21851 logreclem 22332 atans2 22444 basellem3 22538 sqff1o 22638 coltr2 23177 colline 23179 tglowdim2ln 23181 colmid 23210 symquadlem 23211 krippenlem 23212 midexlem 23214 ragperp 23238 mideu 23247 xlt2addrd 26187 eulerpartlemgvv 26895 nobndup 27977 ordtoplem 28417 ordcmp 28429 dvasin 28620 unitresr 29026 acongneg2 29460 unxpwdom3 29588 wallispilem3 30002 hashecclwwlkn1 30648 lkrshp4 33061 2at0mat0 33477 trlator0 34123 dia2dimlem2 35018 dia2dimlem3 35019 dochkrshp 35339 dochkrshp4 35342 lcfl6 35453 lclkrlem2k 35470 hdmap14lem6 35829 hgmapval0 35848 |
Copyright terms: Public domain | W3C validator |