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 4123 acexmidlemcase 5769 poxp 6129 fodjuomnilemdc 7016 indpi 7150 suplocexprlemloc 7529 nneoor 9153 uzp1 9359 maxabslemlub 10979 xrmaxiflemlub 11017 exmidunben 11939 bj-nn0suc 13162 sbthomlem 13220 |
Copyright terms: Public domain | W3C validator |