Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3impb | Unicode version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impb.1 |
Ref | Expression |
---|---|
3impb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impb.1 | . . 3 | |
2 | 1 | exp32 363 | . 2 |
3 | 2 | 3imp 1188 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: 3adant1l 1225 3adant1r 1226 3impdi 1288 vtocl3gf 2793 rspc2ev 2849 reuss 3408 trssord 4365 funtp 5251 resdif 5464 funimass4 5547 fnovex 5886 fnotovb 5896 fovrn 5995 fnovrn 6000 fmpoco 6195 nndi 6465 nnaordi 6487 ecovass 6622 ecoviass 6623 ecovdi 6624 ecovidi 6625 eqsupti 6973 addasspig 7292 mulasspig 7294 distrpig 7295 distrnq0 7421 addassnq0 7424 distnq0r 7425 prcdnql 7446 prcunqu 7447 genpassl 7486 genpassu 7487 genpassg 7488 distrlem1prl 7544 distrlem1pru 7545 ltexprlemopl 7563 ltexprlemopu 7565 le2tri3i 8028 cnegexlem1 8094 subadd 8122 addsub 8130 subdi 8304 submul2 8318 div12ap 8611 diveqap1 8622 divnegap 8623 divdivap2 8641 ltmulgt11 8780 gt0div 8786 ge0div 8787 uzind3 9325 fnn0ind 9328 qdivcl 9602 irrmul 9606 xrlttr 9752 fzen 9999 lenegsq 11059 moddvds 11761 dvds2add 11787 dvds2sub 11788 dvdsleabs 11805 divalgb 11884 ndvdsadd 11890 modgcd 11946 absmulgcd 11972 odzval 12195 pcmul 12255 setsresg 12454 submcl 12701 grpinvid1 12754 grpinvid2 12755 unopn 12797 innei 12957 cncfi 13359 |
Copyright terms: Public domain | W3C validator |