Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3exp | Unicode version |
Description: Exportation inference. (Contributed by NM, 30-May-1994.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3exp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2an3 1160 | . 2 | |
2 | 3exp.1 | . 2 | |
3 | 1, 2 | syl8 71 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 962 |
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 df-3an 964 |
This theorem is referenced by: 3expa 1181 3expb 1182 3expia 1183 3expib 1184 3com23 1187 3an1rs 1197 3exp1 1201 3expd 1202 exp5o 1204 syl3an2 1250 syl3an3 1251 syl2an23an 1277 3impexpbicomi 1415 rexlimdv3a 2551 rabssdv 3177 reupick2 3362 ssorduni 4403 tfisi 4501 fvssunirng 5436 f1oiso2 5728 poxp 6129 tfrlem5 6211 nndi 6382 nnmass 6383 findcard 6782 ac6sfi 6792 mulcanpig 7143 divgt0 8630 divge0 8631 uzind 9162 uzind2 9163 facavg 10492 prodfap0 11314 prodfrecap 11315 dvdsnprmd 11806 prmndvdsfaclt 11834 fiinopn 12171 neipsm 12323 tpnei 12329 opnneiid 12333 neibl 12660 tgqioo 12716 |
Copyright terms: Public domain | W3C validator |