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 362 | . 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: ex3 1190 3impdir 1289 syl3an9b 1305 biimp3a 1340 stoic3 1424 rspec3 2560 rspc3v 2850 raltpg 3636 rextpg 3637 disjiun 3984 otexg 4215 opelopabt 4247 tpexg 4429 3optocl 4689 fun2ssres 5241 funssfv 5522 fvun1 5562 foco2 5733 f1elima 5752 eloprabga 5940 caovimo 6046 ot1stg 6131 ot2ndg 6132 ot3rdgg 6133 brtposg 6233 rdgexggg 6356 rdgivallem 6360 nnmass 6466 nndir 6469 nnaword 6490 th3q 6618 ecovass 6622 ecoviass 6623 fpmg 6652 findcard 6866 unfiin 6903 addasspig 7292 mulasspig 7294 mulcanpig 7297 ltapig 7300 ltmpig 7301 addassnqg 7344 ltbtwnnqq 7377 mulnnnq0 7412 addassnq0 7424 genpassl 7486 genpassu 7487 genpassg 7488 aptiprleml 7601 adddir 7911 le2tri3i 8028 addsub12 8132 subdir 8305 reapmul1 8514 recexaplem2 8570 div12ap 8611 divdiv32ap 8637 divdivap1 8640 lble 8863 zaddcllemneg 9251 fnn0ind 9328 xrltso 9753 iccgelb 9889 elicc4 9897 elfz 9971 fzrevral 10061 expnegap0 10484 expgt0 10509 expge0 10512 expge1 10513 mulexpzap 10516 expp1zap 10525 expm1ap 10526 apexp1 10652 abssubap0 11054 binom 11447 dvds0lem 11763 dvdsnegb 11770 muldvds1 11778 muldvds2 11779 divalgmodcl 11887 gcd2n0cl 11924 lcmdvds 12033 prmdvdsexp 12102 rpexp1i 12108 cnpval 12992 cnf2 12999 cnnei 13026 blssec 13232 blpnfctr 13233 mopni2 13277 mopni3 13278 |
Copyright terms: Public domain | W3C validator |