Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orim2d | Unicode version |
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Ref | Expression |
---|---|
orim1d.1 |
Ref | Expression |
---|---|
orim2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 21 | . 2 | |
2 | orim1d.1 | . 2 | |
3 | 1, 2 | orim12d 775 | 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: orim2 778 orbi2d 779 pm2.82 801 stdcndcOLD 831 pm2.13dc 870 exmid1dc 4118 acexmidlemcase 5762 poxp 6122 fodjuomnilemdc 7009 indpi 7143 suplocexprlemloc 7522 nneoor 9146 uzp1 9352 maxabslemlub 10972 xrmaxiflemlub 11010 exmidunben 11928 bj-nn0suc 13151 sbthomlem 13209 |
Copyright terms: Public domain | W3C validator |