![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orcomd | 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 680 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 120 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: olcd 686 stabtestimpdc 858 pm5.54dc 861 swopo 4096 sotritrieq 4115 reg3exmidlemwe 4356 acexmidlemcase 5584 2oconcl 6133 nntri3or 6184 nntri2 6185 nntri1 6187 nnsseleq 6192 diffisn 6537 djulclb 6652 exmidomniim 6700 exmidomni 6701 addnqprlemfu 7020 mulnqprlemfu 7036 addcanprlemu 7075 cauappcvgprlemladdru 7116 apreap 7962 mulap0r 7990 nnm1nn0 8604 elnn0z 8657 zleloe 8691 nneoor 8742 nneo 8743 zeo2 8746 uzm1 8942 nn01to3 8995 uzsplit 9397 fzospliti 9474 fzouzsplit 9477 qavgle 9557 fz1f1o 10570 zeo3 10646 bezoutlemmain 10765 unennn 10988 |
Copyright terms: Public domain | W3C validator |