Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exp4b | Unicode version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
Ref | Expression |
---|---|
exp4b.1 |
Ref | Expression |
---|---|
exp4b |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4b.1 | . . 3 | |
2 | 1 | ex 108 | . 2 |
3 | 2 | exp4a 348 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: exp43 354 reuss2 3217 nndi 6065 mulnqprl 6666 mulnqpru 6667 distrlem5prl 6684 distrlem5pru 6685 recexprlemss1l 6733 recexprlemss1u 6734 lemul12a 7828 nnmulcl 7935 elfz0fzfz0 8983 fzo1fzo0n0 9039 fzofzim 9044 elfzodifsumelfzo 9057 le2sq2 9329 |
Copyright terms: Public domain | W3C validator |