Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orim12d | Unicode version |
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
Ref | Expression |
---|---|
orim12d.1 | |
orim12d.2 |
Ref | Expression |
---|---|
orim12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orim12d.1 | . 2 | |
2 | orim12d.2 | . 2 | |
3 | pm3.48 699 | . 2 | |
4 | 1, 2, 3 | syl2anc 391 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orim1d 701 orim2d 702 3orim123d 1215 19.33b2 1520 preq12b 3541 prel12 3542 funun 4944 nnsucelsuc 6070 nnaord 6082 nnmord 6090 swoer 6134 fidceq 6330 fin0or 6343 ltsopr 6694 cauappcvgprlemloc 6750 caucvgprlemloc 6773 caucvgprprlemloc 6801 mulextsr1lem 6864 reapcotr 7589 apcotr 7598 mulext1 7603 mulext 7605 peano2z 8281 zeo 8343 uzm1 8503 eluzdc 8547 fzospliti 9032 frec2uzltd 9189 absext 9661 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |