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 1176 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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: 3adant1l 1212 3adant1r 1213 3impdi 1275 vtocl3gf 2775 rspc2ev 2831 reuss 3388 trssord 4340 funtp 5223 resdif 5436 funimass4 5519 fnovex 5854 fnotovb 5864 fovrn 5963 fnovrn 5968 fmpoco 6163 nndi 6433 nnaordi 6455 ecovass 6589 ecoviass 6590 ecovdi 6591 ecovidi 6592 eqsupti 6940 addasspig 7250 mulasspig 7252 distrpig 7253 distrnq0 7379 addassnq0 7382 distnq0r 7383 prcdnql 7404 prcunqu 7405 genpassl 7444 genpassu 7445 genpassg 7446 distrlem1prl 7502 distrlem1pru 7503 ltexprlemopl 7521 ltexprlemopu 7523 le2tri3i 7985 cnegexlem1 8050 subadd 8078 addsub 8086 subdi 8260 submul2 8274 div12ap 8567 diveqap1 8578 divnegap 8579 divdivap2 8597 ltmulgt11 8735 gt0div 8741 ge0div 8742 uzind3 9277 fnn0ind 9280 qdivcl 9552 irrmul 9556 xrlttr 9702 fzen 9945 lenegsq 10995 moddvds 11695 dvds2add 11720 dvds2sub 11721 dvdsleabs 11736 divalgb 11815 ndvdsadd 11821 modgcd 11874 absmulgcd 11900 odzval 12115 setsresg 12228 unopn 12403 innei 12563 cncfi 12965 |
Copyright terms: Public domain | W3C validator |