![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impcom | Unicode version |
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
Ref | Expression |
---|---|
imp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
impcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 27 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 115 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem is referenced by: mpan9 265 19.41h 1572 19.41 1573 equtr2 1594 mopick 1975 2euex 1984 gencl 2580 2gencl 2581 rspccva 2649 sbcimdv 2817 indifdir 3187 sseq0 3252 minel 3277 r19.2m 3303 elelpwi 3362 ssuni 3593 trint0m 3862 ssexg 3887 pofun 4040 sowlin 4048 2optocl 4360 3optocl 4361 elrnmpt1 4528 resieq 4565 fnun 4948 fss 4997 fun 5006 dmfex 5022 fvelimab 5172 mptfvex 5199 fmptco 5273 fnressn 5292 fressnfv 5293 fvtp2g 5313 fvtp3g 5314 fnex 5326 funfvima3 5335 isores3 5398 f1o2ndf1 5791 reldmtpos 5809 smores 5848 tfrlem7 5874 tfrlemi1 5887 tfrexlem 5889 rdgon 5913 frecrdg 5931 nnacl 5998 nnmcl 5999 nnmsucr 6006 nntri3or 6011 nnaword 6020 nnaordex 6036 2ecoptocl 6130 enm 6230 elni2 6298 ax1rid 6761 mulgt1 7610 nnaddcl 7715 nnmulcl 7716 zaddcllempos 8058 zaddcllemneg 8060 nn0n0n1ge2b 8096 fzind 8129 fnn0ind 8130 uzaddcl 8305 uzsubsubfz 8681 elfz1b 8722 elfz0ubfz0 8752 fz0fzdiffz0 8757 elfzmlbmOLD 8759 elfzmlbp 8760 fzofzim 8814 elfzom1elp1fzo 8828 elfzom1p1elfzo 8840 ssfzo12bi 8851 expivallem 8910 expcllem 8920 expap0 8939 cjexp 9121 bdssexg 9359 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |