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 363 | 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 369 reuss2 3326 nndi 6350 mulnqprl 7344 mulnqpru 7345 distrlem5prl 7362 distrlem5pru 7363 recexprlemss1l 7411 recexprlemss1u 7412 lemul12a 8588 nnmulcl 8709 elfz0fzfz0 9871 fzo1fzo0n0 9928 fzofzim 9933 elfzodifsumelfzo 9946 le2sq2 10336 oddprmgt2 11741 |
Copyright terms: Public domain | W3C validator |