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 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: 3impdir 1276 syl3an9b 1292 biimp3a 1327 stoic3 1411 rspec3 2547 rspc3v 2832 raltpg 3612 rextpg 3613 disjiun 3960 otexg 4190 opelopabt 4222 tpexg 4404 3optocl 4664 fun2ssres 5213 funssfv 5494 fvun1 5534 foco2 5704 f1elima 5723 eloprabga 5908 caovimo 6014 ot1stg 6100 ot2ndg 6101 ot3rdgg 6102 brtposg 6201 rdgexggg 6324 rdgivallem 6328 nnmass 6434 nndir 6437 nnaword 6458 th3q 6585 ecovass 6589 ecoviass 6590 fpmg 6619 findcard 6833 unfiin 6870 addasspig 7250 mulasspig 7252 mulcanpig 7255 ltapig 7258 ltmpig 7259 addassnqg 7302 ltbtwnnqq 7335 mulnnnq0 7370 addassnq0 7382 genpassl 7444 genpassu 7445 genpassg 7446 aptiprleml 7559 adddir 7869 le2tri3i 7985 addsub12 8088 subdir 8261 reapmul1 8470 recexaplem2 8526 div12ap 8567 divdiv32ap 8593 divdivap1 8596 lble 8818 zaddcllemneg 9206 fnn0ind 9280 xrltso 9703 iccgelb 9836 elicc4 9844 elfz 9918 fzrevral 10007 expnegap0 10427 expgt0 10452 expge0 10455 expge1 10456 mulexpzap 10459 expp1zap 10468 expm1ap 10469 apexp1 10592 abssubap0 10990 binom 11381 dvds0lem 11697 dvdsnegb 11704 muldvds1 11712 muldvds2 11713 divalgmodcl 11819 gcd2n0cl 11853 lcmdvds 11956 prmdvdsexp 12023 rpexp1i 12029 cnpval 12609 cnf2 12616 cnnei 12643 blssec 12849 blpnfctr 12850 mopni2 12894 mopni3 12895 |
Copyright terms: Public domain | W3C validator |