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 114 | . 2 |
3 | 2 | exp4a 364 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exp43 370 reuss2 3407 nndi 6465 mulnqprl 7530 mulnqpru 7531 distrlem5prl 7548 distrlem5pru 7549 recexprlemss1l 7597 recexprlemss1u 7598 lemul12a 8778 nnmulcl 8899 elfz0fzfz0 10082 fzo1fzo0n0 10139 fzofzim 10144 elfzodifsumelfzo 10157 le2sq2 10551 oddprmgt2 12088 infpnlem1 12311 |
Copyright terms: Public domain | W3C validator |