![]() |
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 700 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 121 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 681 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: olcd 706 stdcndcOLD 814 pm5.54dc 884 exmid1dc 4081 swopo 4186 sotritrieq 4205 reg3exmidlemwe 4451 acexmidlemcase 5721 2oconcl 6288 nntri3or 6341 nntri2 6342 nntri1 6344 nnsseleq 6349 diffisn 6738 fival 6808 djulclb 6890 exmidomniim 6961 exmidomni 6962 addnqprlemfu 7310 mulnqprlemfu 7326 addcanprlemu 7365 cauappcvgprlemladdru 7406 apreap 8261 mulap0r 8289 mul0eqap 8338 nnm1nn0 8916 elnn0z 8965 zleloe 8999 nneoor 9051 nneo 9052 zeo2 9055 uzm1 9252 nn01to3 9305 uzsplit 9759 fzospliti 9840 fzouzsplit 9843 qavgle 9923 xrmaxiflemlub 10903 fz1f1o 11030 ef0lem 11211 zeo3 11407 bezoutlemmain 11526 unennn 11749 exmidunben 11778 nninfalllem1 12884 nninfall 12885 nninfsellemqall 12892 exmidsbthrlem 12898 sbthomlem 12901 trilpolemeq1 12914 |
Copyright terms: Public domain | W3C validator |