Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3impa | Unicode version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impa.1 |
Ref | Expression |
---|---|
3impa |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impa.1 | . . 3 | |
2 | 1 | exp31 361 | . 2 |
3 | 2 | 3imp 1160 | 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: 3impdir 1257 syl3an9b 1273 biimp3a 1308 stoic3 1392 rspec3 2499 rspc3v 2779 raltpg 3546 rextpg 3547 disjiun 3894 otexg 4122 opelopabt 4154 tpexg 4335 3optocl 4587 fun2ssres 5136 funssfv 5415 fvun1 5455 foco2 5623 f1elima 5642 eloprabga 5826 caovimo 5932 ot1stg 6018 ot2ndg 6019 ot3rdgg 6020 brtposg 6119 rdgexggg 6242 rdgivallem 6246 nnmass 6351 nndir 6354 nnaword 6375 th3q 6502 ecovass 6506 ecoviass 6507 fpmg 6536 findcard 6750 unfiin 6782 addasspig 7106 mulasspig 7108 mulcanpig 7111 ltapig 7114 ltmpig 7115 addassnqg 7158 ltbtwnnqq 7191 mulnnnq0 7226 addassnq0 7238 genpassl 7300 genpassu 7301 genpassg 7302 aptiprleml 7415 adddir 7725 le2tri3i 7840 addsub12 7943 subdir 8116 reapmul1 8325 recexaplem2 8381 div12ap 8422 divdiv32ap 8448 divdivap1 8451 lble 8673 zaddcllemneg 9061 fnn0ind 9135 xrltso 9550 iccgelb 9683 elicc4 9691 elfz 9764 fzrevral 9853 expnegap0 10269 expgt0 10294 expge0 10297 expge1 10298 mulexpzap 10301 expp1zap 10310 expm1ap 10311 abssubap0 10830 binom 11221 dvds0lem 11430 dvdsnegb 11437 muldvds1 11445 muldvds2 11446 divalgmodcl 11552 gcd2n0cl 11585 lcmdvds 11687 prmdvdsexp 11753 rpexp1i 11759 cnpval 12294 cnf2 12301 cnnei 12328 blssec 12534 blpnfctr 12535 mopni2 12579 mopni3 12580 |
Copyright terms: Public domain | W3C validator |