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 717 | . 2 | |
3 | 1, 2 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: olcd 723 stdcndcOLD 831 pm5.54dc 903 exmid1dc 4118 swopo 4223 sotritrieq 4242 reg3exmidlemwe 4488 acexmidlemcase 5762 2oconcl 6329 nntri3or 6382 nntri2 6383 nntri1 6385 nnsseleq 6390 diffisn 6780 fival 6851 djulclb 6933 exmidomniim 7006 exmidomni 7007 addnqprlemfu 7361 mulnqprlemfu 7377 addcanprlemu 7416 cauappcvgprlemladdru 7457 apreap 8342 mulap0r 8370 mul0eqap 8424 nnm1nn0 9011 elnn0z 9060 zleloe 9094 nneoor 9146 nneo 9147 zeo2 9150 uzm1 9349 nn01to3 9402 uzsplit 9865 fzospliti 9946 fzouzsplit 9949 qavgle 10029 xrmaxiflemlub 11010 fz1f1o 11137 ef0lem 11355 zeo3 11554 bezoutlemmain 11675 unennn 11899 exmidunben 11928 nninfalllem1 13192 nninfall 13193 nninfsellemqall 13200 exmidsbthrlem 13206 sbthomlem 13209 trilpolemeq1 13222 |
Copyright terms: Public domain | W3C validator |