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 864 | . 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓)) | |
3 | 1, 2 | sylib 219 | 1 ⊢ (𝜑 → (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: unitresr 867 olcd 870 19.33b 1877 r19.30 3335 swopo 5477 fr2nr 5526 ordtri1 6217 ordequn 6284 ssonprc 7496 ordunpr 7530 ordunisuc2 7548 2oconcl 8117 erdisj 8330 ordtypelem7 8976 ackbij1lem18 9647 fin23lem19 9746 gchi 10034 inar1 10185 inatsk 10188 avgle 11867 nnm1nn0 11926 zle0orge1 11986 uzsplit 12967 fzospliti 13057 fzouzsplit 13060 znsqcld 13514 fz1f1o 15055 fnpr2ob 16819 odcl 18593 gexcl 18634 lssvs0or 19811 lspdisj 19826 lspsncv0 19847 mdetralt 21145 filconn 22419 limccnp 24416 dgrlt 24783 logreclem 25267 atans2 25436 basellem3 25587 sqff1o 25686 tgcgrsub2 26308 legov3 26311 colline 26362 tglowdim2ln 26364 mirbtwnhl 26393 colmid 26401 symquadlem 26402 midexlem 26405 ragperp 26430 colperp 26442 midex 26450 oppperpex 26466 hlpasch 26469 colopp 26482 lmieu 26497 lmicom 26501 lmimid 26507 lmiisolem 26509 trgcopy 26517 cgracgr 26531 cgraswap 26533 cgracol 26541 hashecclwwlkn1 27783 xlt2addrd 30408 fprodex01 30468 lvecdim0 30904 esumcvgre 31249 ordtoplem 33680 ordcmp 33692 onsucuni3 34530 dvasin 34859 eqvreldisj 35729 lkrshp4 36124 2at0mat0 36541 trlator0 37187 dia2dimlem2 38081 dia2dimlem3 38082 dochkrshp 38402 dochkrshp4 38405 lcfl6 38516 lclkrlem2k 38533 hdmap14lem6 38889 hgmapval0 38908 acongneg2 39452 unxpwdom3 39573 mnuprdlem1 40485 mnurndlem1 40494 elunnel2 41173 disjinfi 41330 xrssre 41492 icccncfext 42046 wallispilem3 42229 fourierdlem93 42361 fourierdlem101 42369 nneop 44514 itsclinecirc0 44688 itsclinecirc0b 44689 itsclinecirc0in 44690 inlinecirc02plem 44701 inlinecirc02p 44702 |
Copyright terms: Public domain | W3C validator |