Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impancom | Unicode version |
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.) |
Ref | Expression |
---|---|
impancom.1 |
Ref | Expression |
---|---|
impancom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impancom.1 | . . . 4 | |
2 | 1 | ex 114 | . . 3 |
3 | 2 | com23 78 | . 2 |
4 | 3 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 is referenced by: eqrdav 2116 disjiun 3894 euotd 4146 onsucelsucr 4394 isotr 5685 spc2ed 6098 ltbtwnnqq 7191 genpcdl 7295 genpcuu 7296 un0addcl 8978 un0mulcl 8979 btwnnz 9113 uznfz 9851 elfz0ubfz0 9870 fzoss1 9916 elfzo0z 9929 fzofzim 9933 elfzom1p1elfzo 9959 ssfzo12bi 9970 subfzo0 9987 modfzo0difsn 10136 expaddzap 10305 caucvgre 10721 caubnd2 10857 summodc 11120 fzo0dvdseq 11482 nno 11530 lcmdvds 11687 hashgcdeq 11831 neii1 12243 neii2 12245 fsumcncntop 12652 |
Copyright terms: Public domain | W3C validator |