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 3387 nndi 6433 mulnqprl 7488 mulnqpru 7489 distrlem5prl 7506 distrlem5pru 7507 recexprlemss1l 7555 recexprlemss1u 7556 lemul12a 8733 nnmulcl 8854 elfz0fzfz0 10025 fzo1fzo0n0 10082 fzofzim 10087 elfzodifsumelfzo 10100 le2sq2 10494 oddprmgt2 12011 |
Copyright terms: Public domain | W3C validator |