![]() |
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 1161 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3exp.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl8 71 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 965 |
This theorem is referenced by: 3expa 1182 3expb 1183 3expia 1184 3expib 1185 3com23 1188 3an1rs 1198 3exp1 1202 3expd 1203 exp5o 1205 syl3an2 1251 syl3an3 1252 syl2an23an 1278 3impexpbicomi 1416 rexlimdv3a 2554 rabssdv 3182 reupick2 3367 ssorduni 4411 tfisi 4509 fvssunirng 5444 f1oiso2 5736 poxp 6137 tfrlem5 6219 nndi 6390 nnmass 6391 findcard 6790 ac6sfi 6800 mulcanpig 7167 divgt0 8654 divge0 8655 uzind 9186 uzind2 9187 facavg 10524 prodfap0 11346 prodfrecap 11347 dvdsnprmd 11842 prmndvdsfaclt 11870 fiinopn 12210 neipsm 12362 tpnei 12368 opnneiid 12372 neibl 12699 tgqioo 12755 |
Copyright terms: Public domain | W3C validator |