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 2156 disjiun 3962 euotd 4216 onsucelsucr 4469 isotr 5768 spc2ed 6182 ltbtwnnqq 7337 genpcdl 7441 genpcuu 7442 un0addcl 9128 un0mulcl 9129 btwnnz 9263 uznfz 10011 elfz0ubfz0 10033 fzoss1 10079 elfzo0z 10092 fzofzim 10096 elfzom1p1elfzo 10122 ssfzo12bi 10133 subfzo0 10150 modfzo0difsn 10303 expaddzap 10472 caucvgre 10892 caubnd2 11028 summodc 11291 fzo0dvdseq 11761 nno 11809 lcmdvds 11971 hashgcdeq 12129 modprm0 12144 neii1 12617 neii2 12619 fsumcncntop 13026 |
Copyright terms: Public domain | W3C validator |