![]() |
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 868 | . 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓)) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 |
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 846 |
This theorem is referenced by: olcd 872 orcnd 876 19.33b 1880 r19.30OLD 3110 elunnel2 4147 swopo 5601 fr2nr 5656 ordtri1 6404 ordequn 6474 ssonprc 7791 ordunpr 7830 ordunisuc2 7849 2oconcl 8524 erdisj 8778 ordtypelem7 9554 ackbij1lem18 10267 fin23lem19 10366 gchi 10654 inar1 10805 inatsk 10808 avgle 12492 nnm1nn0 12551 zle0orge1 12613 uzsplit 13613 fzospliti 13704 fzouzsplit 13707 znsqcld 14167 fz1f1o 15697 fnpr2ob 17548 odcl 19508 gexcl 19552 lssvs0or 21015 lspdisj 21030 lspsncv0 21051 mdetralt 22559 filconn 23836 limccnp 25869 dgrlt 26251 logreclem 26744 atans2 26913 basellem3 27065 sqff1o 27164 nosep2o 27666 elnns2 28266 tgcgrsub2 28476 legov3 28479 colline 28530 tglowdim2ln 28532 mirbtwnhl 28561 colmid 28569 symquadlem 28570 midexlem 28573 ragperp 28598 colperp 28610 midex 28618 oppperpex 28634 hlpasch 28637 colopp 28650 lmieu 28665 lmicom 28669 lmimid 28675 lmiisolem 28677 trgcopy 28685 cgracgr 28699 cgraswap 28701 cgracol 28709 hashecclwwlkn1 29964 xlt2addrd 32615 fprodex01 32678 ssmxidl 33291 drngmxidlr 33295 lvecdim0 33437 minplyirred 33514 irredminply 33517 zarclssn 33607 esumcvgre 33843 ordtoplem 36052 ordcmp 36064 onsucuni3 36979 dvasin 37310 eqvreldisj 38218 lkrshp4 38712 2at0mat0 39130 trlator0 39776 dia2dimlem2 40670 dia2dimlem3 40671 dochkrshp 40991 dochkrshp4 40994 lcfl6 41105 lclkrlem2k 41122 hdmap14lem6 41478 hgmapval0 41497 sticksstones12a 41762 sticksstones13 41764 acongneg2 42542 unxpwdom3 42663 dflim5 42902 mnuprdlem1 43853 mnurndlem1 43862 disjinfi 44706 xrssre 44870 icccncfext 45415 wallispilem3 45595 fourierdlem93 45727 fourierdlem101 45735 nneop 47787 itsclinecirc0 48034 itsclinecirc0b 48035 itsclinecirc0in 48036 inlinecirc02plem 48047 inlinecirc02p 48048 |
Copyright terms: Public domain | W3C validator |