![]() |
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 1176 |
. 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 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3expa 1203 3expb 1204 3expia 1205 3expib 1206 3com23 1209 3an1rs 1219 3exp1 1223 3expd 1224 exp5o 1226 syl3an2 1272 syl3an3 1273 syl2an23an 1299 3impexpbicomi 1439 rexlimdv3a 2596 rabssdv 3235 reupick2 3421 ssorduni 4485 tfisi 4585 fvssunirng 5529 f1oiso2 5825 poxp 6230 tfrlem5 6312 nndi 6484 nnmass 6485 findcard 6885 ac6sfi 6895 mulcanpig 7331 divgt0 8825 divge0 8826 uzind 9360 uzind2 9361 facavg 10719 prodfap0 11546 prodfrecap 11547 fprodabs 11617 dvdsmodexp 11795 dvdsnprmd 12117 prmndvdsfaclt 12148 fermltl 12226 pceu 12287 mulgass2 13166 fiinopn 13373 neipsm 13525 tpnei 13531 opnneiid 13535 neibl 13862 tgqioo 13918 |
Copyright terms: Public domain | W3C validator |