Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3expb | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3expb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3exp 1165 | . 2 |
3 | 2 | imp32 255 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
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 949 |
This theorem is referenced by: 3adant3r1 1175 3adant3r2 1176 3adant3r3 1177 3adant1l 1193 3adant1r 1194 mp3an1 1287 soinxp 4579 sotri 4904 fnfco 5267 mpoeq3dva 5803 fovrnda 5882 ovelrn 5887 grprinvd 5934 fnmpoovd 6080 nnmsucr 6352 fidifsnid 6733 exmidpw 6770 undiffi 6781 fidcenumlemim 6808 ltpopr 7371 ltexprlemdisj 7382 recexprlemdisj 7406 mul4 7862 add4 7891 2addsub 7944 addsubeq4 7945 subadd4 7974 muladd 8114 ltleadd 8176 divmulap 8403 divap0 8412 div23ap 8419 div12ap 8422 divsubdirap 8436 divcanap5 8442 divmuleqap 8445 divcanap6 8447 divdiv32ap 8448 div2subap 8564 letrp1 8574 lemul12b 8587 lediv1 8595 cju 8687 nndivre 8724 nndivtr 8730 nn0addge1 8991 nn0addge2 8992 peano2uz2 9126 uzind 9130 uzind3 9132 fzind 9134 fnn0ind 9135 uzind4 9351 qre 9385 irrmul 9407 rpdivcl 9435 rerpdivcl 9440 iccshftr 9745 iccshftl 9747 iccdil 9749 icccntr 9751 fzaddel 9807 fzrev 9832 frec2uzf1od 10147 expdivap 10312 2shfti 10571 iooinsup 11014 isermulc2 11077 dvds2add 11454 dvds2sub 11455 dvdstr 11457 alzdvds 11479 divalg2 11550 lcmgcdlem 11685 lcmgcdeq 11691 isprm6 11752 tgclb 12161 topbas 12163 neissex 12261 cnpnei 12315 txcnp 12367 psmetxrge0 12428 psmetlecl 12430 xmetlecl 12463 xmettpos 12466 elbl3ps 12490 elbl3 12491 metss 12590 comet 12595 bdxmet 12597 bdmet 12598 bl2ioo 12638 divcnap 12651 cncffvrn 12665 divccncfap 12673 dvrecap 12773 cosz12 12788 |
Copyright terms: Public domain | W3C validator |