![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orcomd | Structured version Visualization version GIF 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 869 | . 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓)) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: olcd 873 orcnd 878 19.33b 1889 r19.30OLD 3123 elunnel2 4109 swopo 5555 fr2nr 5610 ordtri1 6349 ordequn 6419 ssonprc 7715 ordunpr 7754 ordunisuc2 7773 2oconcl 8442 erdisj 8659 ordtypelem7 9419 ackbij1lem18 10132 fin23lem19 10231 gchi 10519 inar1 10670 inatsk 10673 avgle 12354 nnm1nn0 12413 zle0orge1 12475 uzsplit 13468 fzospliti 13559 fzouzsplit 13562 znsqcld 14020 fz1f1o 15555 fnpr2ob 17400 odcl 19277 gexcl 19321 lssvs0or 20524 lspdisj 20539 lspsncv0 20560 mdetralt 21909 filconn 23186 limccnp 25207 dgrlt 25579 logreclem 26064 atans2 26233 basellem3 26384 sqff1o 26483 nosep2o 26982 tgcgrsub2 27366 legov3 27369 colline 27420 tglowdim2ln 27422 mirbtwnhl 27451 colmid 27459 symquadlem 27460 midexlem 27463 ragperp 27488 colperp 27500 midex 27508 oppperpex 27524 hlpasch 27527 colopp 27540 lmieu 27555 lmicom 27559 lmimid 27565 lmiisolem 27567 trgcopy 27575 cgracgr 27589 cgraswap 27591 cgracol 27599 hashecclwwlkn1 28850 xlt2addrd 31488 fprodex01 31546 ssmxidl 32059 lvecdim0 32118 zarclssn 32258 esumcvgre 32494 ordtoplem 34839 ordcmp 34851 onsucuni3 35770 dvasin 36094 eqvreldisj 37008 lkrshp4 37502 2at0mat0 37920 trlator0 38566 dia2dimlem2 39460 dia2dimlem3 39461 dochkrshp 39781 dochkrshp4 39784 lcfl6 39895 lclkrlem2k 39912 hdmap14lem6 40268 hgmapval0 40287 sticksstones12a 40497 sticksstones13 40499 acongneg2 41204 unxpwdom3 41325 dflim5 41564 mnuprdlem1 42457 mnurndlem1 42466 disjinfi 43311 xrssre 43481 icccncfext 44023 wallispilem3 44203 fourierdlem93 44335 fourierdlem101 44343 nneop 46507 itsclinecirc0 46754 itsclinecirc0b 46755 itsclinecirc0in 46756 inlinecirc02plem 46767 inlinecirc02p 46768 |
Copyright terms: Public domain | W3C validator |